A Design Discipline and Language Features
       for Formal Modular Reasoning in Aspect-Oriented Programs
				  by
		  Curtis Clifton and Gary T. Leavens

			       Abstract

Advice in aspect-oriented programming helps programmers modularize
crosscutting concerns by allowing additions and changes to a
program's execution.  However, formal reasoning about the functional
behavior of aspect-oriented programs requires a non-modular,
whole-program search to find applicable advice.

To allow modular reasoning, we describe a discipline that
categorizes aspects into two sorts: spectators and
assistants. "Spectators" are statically checked to not modify the
behavior of the code they advise; this restriction lets them remain
unseen.  Unlike spectators, "assistants" are not restricted in their
behavior. However, for modular reasoning one must be able to identify
all applicable assistants, hence assistants must be explicitly
accepted by the code they advise.  Besides allowing modular reasoning,
this discipline permits the use of existing idioms, and appears to be
statically verifiable and practical for software development.
Indeed, expert aspect-oriented programmers seem to use such a discipline.

Keywords: Spectators, assistants, aspect-oriented programming,
modular reasoning, AspectJ language.

2002 CR Categories: 
D.3.1 [Programming Languages]
 	Programming Techniques --- Object-oriented programming,
        aspect-oriented programming;
D.3.2 [Programming Languages]
	Language Classifications --- Object-oriented languages, Java, AspectJ;
D.3.3 [Programming Languages]
	Language Constructs and Features --- control structures,
        modules, packages, procedures, functions and subroutines, advice,
        spectators, assistants, aspects;

Submitted for publication