archives

A design discipline and language features for modular reasoning in aspect-oriented programs


Home 

About 

Browse 

Search 

Register 

Subscriptions 

Deposit Papers 

Help
    

Clifton, Curtis (2005) A design discipline and language features for modular reasoning in aspect-oriented programs. Technical Report 05-15, Computer Science, Iowa State University.

Full text available as:Adobe PDF

Abstract

Aspect-oriented programming lets programmers modularize concerns that are orthogonal to the main decomposition of a program. To do this, aspect-oriented programming includes modules called aspects that may modify the behavior, or advise, code in the main decomposition. Aspect-oriented programming also allows aspects to declaratively specify what code should be advised. This means that a whole-program search is required to find all the aspects that might advise a given piece of code. The problems this causes are somewhat analogous to overriding methods and polymorphic method dispatch in traditional object-oriented programming.

In object-oriented programming, the discipline of behavioral subtyping permits reasoning about polymorphic methods even when overriding methods remain unseen. The discipline gives guidance to the author of an overriding method: the overriding method must satisfy the specification of the overridden, superclass method. If the author follows the discipline, then other programmers can reason about a method invocation based on the specification of the superclass method, even if an unseen overriding method might actually be executed.

This dissertation describes an analogous discipline for aspect-oriented programming. The basic premise is that modular reasoning about aspect-oriented programs requires shared responsibility between the aspect author and the client programmer, whose code might be advised by the aspect.

To mediate this sharing, this dissertation proposes that aspects be categorized into two sorts: “spectators” and “assistants”. Spectators are statically restricted to not modify the behavior of the code that they advise. Because of their restricted behavior, spectators may remain unseen by the client programmer. The burden is on the aspect programmer to ensure that spectators satisfy their restrictions. Unlike spectators, assistants are not restricted in their behavior. The burden of reasoning about their effects falls to the client programmer. To do this, the client programmer must be able to identify all applicable assistants. Thus, assistants must be explicitly accepted by the advised code. This discipline allows modular reasoning, permits the use of existing aspect-oriented idioms, and appears to be practical and statically verifiable. A formal study demonstrates that the restrictions on spectators may be statically checked.

Keywords:MAO discipline, MiniMAO calculus, aspect-oriented programming, AspectJ, spectators, assistants, AspectJML, modular reasoning
Subjects:Software: PROGRAMMING TECHNIQUES (E): Object-oriented Programming
Software: PROGRAMMING LANGUAGES: Formal Definitions and Theory (D.2.1, F.3.1-2, F.4.2-3)
Software: PROGRAMMING LANGUAGES: Language Classifications
ID code:00000374
Deposited by:Curtis Clifton on 19 July 2005



Contact site administrator at: ssg@cs.iastate.edu