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

作     者：Clifton, Curtis Leavens, Gary T. 

作者机构：Rose Hulman Inst Technol Dept Comp Sci & Software Engn Terre Haute IN 47803 USA Iowa State Univ Dept Comp Sci Ames IA 50010 USA 

出 版 物：《SCIENCE OF COMPUTER PROGRAMMING》 (计算机程序设计科学)

年 卷 期：2006年第63卷第3期

页      面：321-374页

核心收录：

学科分类：08[工学] 0835[工学-软件工程] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

基　　金：National Science Foundation  NSF  (CCF-04-8078) 

主　　题：aspect-oriented programming MiniMAO calculus formal semantics 

摘      要：This paper describes MiniMAO(1), a core aspect-oriented language. Unlike previous aspect-oriented calculi and core languages, MiniMAO(1) allows around advice to change the target object of an advised operation before proceeding. MiniMAO(1) accurately 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. MiniMAO(1) was designed to serve as a core language for studying modular specification and verification in the aspect-oriented paradigm. To this end MiniMAO(1) center dot has an imperative, reference-based semantics, center dot models the control-flow effects of changing target object bindings with advice, and center dot has a safe static type system. The first two features make MiniMAO(1) 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(1) uses 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 MiniMAO(1). (c) 2006 Elsevier B.V. All rights reserved.