Graph-based specification and simulation of featherweight Java with around advice

ABSTRACT

In this paper we specify an operational run-time semantics of Assignment Featherweight Java -- a minimal subset of Java with assignments -- with around advice, using graph transformations. We introduce a notion of correctness of our specification with respect to an existing semantics and claim a number of advantages over traditional mathematical notations, that come forth from the executable nature of graph-transformation-based semantics.

Using test programs as graphs during specification of the semantics, simulation can help in verifying the correctness of the rules simply by testing, increasing the rigorousness of the specification process. Also, execution of the semantics results in a state space that can be used for analysis and verification, giving rise to an effective method for aspect program verification.

As a criterion for correctness, we use a structural operational semantics of this language from the so-called Common Aspect Semantics Base.

REFERENCES

• 1: Mehmet Aksit , Arend Rensink , Tom Staijen, A graph-transformation-based simulation approach for analysing aspect interference on shared join points, Proceedings of the 8th ACM international conference on Aspect-oriented software development, March 02-06, 2009, Charlottesville, Virginia, USA [doi>10.1145/1509239.1509247]
• 2: Remi Douence, Simplice Djoko Djoko, Pascal Fradet, and Didier Le Botlan. Towards a common aspect semantic base (casb). In Deliverable 54, AOSD-Europe, EU Network of Excellence in AOSD, August 2006.
• 3: Atsushi Igarashi , Benjamin C. Pierce , Philip Wadler, Featherweight Java: a minimal core calculus for Java and GJ, ACM Transactions on Programming Languages and Systems (TOPLAS), v.23 n.3, p.396-450, May 2001 [doi>10.1145/503502.503505]
• 4: H. Kastenberg, A. G. Kleppe, and A. Rensink. Engineering object-oriented semantics using graph transformations. Technical Report TR-CTIT-06-12, University of Twente, Enschede, March 2006.
• 5: H. Kastenberg and A. Rensink. Model checking dynamic states in groove. In A. Valmari, editor, Model Checking Software (SPIN), Vienna, Austria, volume 3925 of Lecture Notes in Computer Science, pages 299--305, Berlin, 2006. Springer-Verlag.
• 6: Gregor Kiczales, John Lamping, Anurag Mendhekar, Chris Maeda, Cristina Videira Lopes, Jean-Marc Loingtier, and John Irwin. Aspect-oriented programming. In ECOOP, pages 220--242, 1997.
• 7: Thomas Mølhave and Lars H. Peterseny. Assignment featherweight java: Bringing mutable state to featherweight java. Master's thesis, University of Aarhus, 2005.
• 8: Arend Rensink. The GROOVE simulator: A tool for state space generation. In J. Pfalz, M. Nagl, and B. Böhlen, editors, Applications of Graph Transformations with Industrial Relevance (AGTIVE), volume 3062 of Lecture Notes in Computer Science, pages 479--485. Springer-Verlag, 2004.
• 9: Grzegorz Rozenberg, Handbook of graph grammars and computing by graph transformation: volume I. foundations, World Scientific Publishing Co., Inc., River Edge, NJ, 1997

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Operational semantics

General Terms:
Languages, Theory

Keywords:
graph transformations, simulation, verification