Reasoning about the Behavior of Aspect-Oriented Programs

Aspect-oriented programming (AOP) has become increasingly popular over the last few years. At the same time, reasoning about the behavior of these programs poses serious challenges. In this paper, we present a rely-guarantee approach to such reasoning. The rely-guarantee approach has proven useful in reasoning about concurrent and distributed programs. We show that some of the key problems encountered in reasoning about aspect-oriented programs are similar to those encountered in reasoning about concurrent programs; and that the rely-guarantee approach, appropriately modified, helps address these problems. We illustrate our approach with a simple example