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.