This page describes work originally carried out under NSF grant CCF-04-8078 on semantics and reasoning for aspect-oriented programs. The principal investigator was Gary T. Leavens, and much of the research was being carried out by Curtis Clifton (who was a Ph.D. student during the grant period). Since then professors Clifton and Leavens have continued to collaborate on this topic, and it has also involved collaboration with James Noble and Hridesh Rajan. The work with Prof. Rajan has been partially supported under NSF grants CNS-0627354, CCF-0429567, CNS-07-09217, CNS 08-08913, CCF-10-17262, and CCF-1017334.

Overview

This project aims to advance the theory and practice of aspect-oriented software development. Like polymorphic method invocation in object-oriented programming, aspect-oriented programming achieves its advances in code modularization by means of additional indirection at run time. Aspect-oriented languages allow the declarative insertion of code at multiple, arbitrary points in the execution of a program. The arbitrary and declarative nature of this indirection means that one must, in general, have whole-program knowledge to reason about the dynamic execution of an aspect-oriented program.

How can one efficiently do static reasoning about a program's execution in the face of such global indirection? In object-oriented programming this concern is addressed through the discipline of behavioral subtyping. Behavioral subtyping places a constraint on subtype programmers: overriding methods in a subtype must satisfy the specification of the overridden supertype methods. In exchange for programming within this constraint, clients of the supertype may efficiently reason about message sends to supertype instances without worrying about the effects of overriding methods in unseen subtypes. Such a discipline allows programmers to reason abstractly about a message send in terms of the receiver's static type. Using the discipline of behavioral subtyping, one can recover static, modular reasoning, while enjoying all of the object-oriented paradigm's code modularization benefits.

The problem addressed by this project is how to efficiently do static reasoning in aspect-oriented programs, while retaining most of the new paradigm's code benefits in terms of decreased scattering and tangling. The project aims to identify a design discipline for aspect-oriented programming that solves this problem. Such a design discipline must deal with the multi-dimensional separation of concerns enabled by aspect-oriented features.

The technical approach will be to create the design discipline, using an analogy to behavioral subtyping, and a small aspect-oriented programming language to support it. By producing prototype tools and applying them in case studies, the researchers will experimentally validate the utility of the language and design discipline. A formal study of specification and verification techniques will demonstrate soundness of static, modular reasoning in the language and design discipline.

Papers

The following papers are related to the project. They are listed in reverse chronological order.

Talks

Gary T. Leavens gave a talk "Concerning Efficient Reasoning in AspectJ-like Languages" at the Aspects, Dependencies and Interactions (ADI) 2007 workshop in Berlin on July 30, 2007. You may be interested in seeing Gary's slides (in PDF format) or his talk's abstract.

Gary T. Leavens was the "discussant" at OOPSLA 2006 for Friedrich Steimann's essay "The Paradoxical Success of Aspect-Oriented Programming" (OOPSLA 2006 Proceedings). You may be interested in seeing Gary's slides (in PDF format).
A paper that reflects some of the points of Gary's discussion is TR07-01a (see above).

Other

See the Ptolemy website for more about the Ptolemy language.

See also Curtis Clifton's web page and Gary T. Leavens's research page for less directly related publications.

Last update $Date: 2022/08/18 01:35:44 $