MiniMAO₁ : An imperative core language for studying aspect-oriented reasoning

详细信息    查看全文

• 作者：Curtis Clifton and Gary T. Leavens
• 关键词：Aspect-oriented programming ; MiniMAO calculus ; Formal semantics
• 刊名：Science of Computer Programming
• 出版年：2006
• 出版时间：15 December 2006
• 年：2006
• 卷：63
• 期：3
• 页码：321-374
• 全文大小：765 K

文摘

This paper describes MiniMAO₁, a core aspect-oriented language. Unlike previous aspect-oriented calculi and core languages, MiniMAO₁allows <tt>aroundtt> advice to change the target object of an advised operation before proceeding. MiniMAO₁accurately models the ways AspectJ allows changing the target object, e.g., at <tt>calltt> join points. Practical uses for changing the target object using advice include proxies and other wrapper objects.

MiniMAO₁was designed to serve as a core language for studying modular specification and verification in the aspect-oriented paradigm. To this end MiniMAO₁

t>

• has an imperative, reference-based semantics,t>t>

• models the control-flow effects of changing target object bindings with advice, andt>t>

• has a safe static type system.t>

The first two features make MiniMAO₁ 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 MiniMAO₁uses a slightly different form of <tt>proceedtt> 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 MiniMAO₁.