MiniMAO1 : An imperative core language for studying aspect-oriented reasoning

This paper describes MiniMAO1, a core aspect-oriented language. Unlike previous aspect-oriented calculi and core languages, MiniMAO1allows around advice to change the target object of an advised operation before proceeding. MiniMAO1accurately models the ways AspectJ allows changing the target object, e.g., at call join points. Practical uses for changing the target object using advice include proxies and other wrapper objects. MiniMAO1was designed to serve as a core language for studying modular specification and verification in the aspect-oriented paradigm. To this end MiniMAO1 • has an imperative, reference-based semantics, • models the control-flow effects of changing target object bindings with advice, and • has a safe static type system. The first two features make MiniMAO1 suitable for the study of aspect-oriented mechanisms, such as those found in AspectJ. These features are important for studying the interaction of aspect-oriented language features with modular specification and verification. A statically type-safe language is also important for such research. AspectJ does not have a safe static type system. To achieve static type safety MiniMAO1uses a slightly different form of proceed and advice binding than in AspectJ. These changes are sufficient for static type safety, but we do not claim that they are necessary; a less restrictive type system might suffice. This paper gives an operational semantics, type system, and proof of soundness for MiniMAO1.