Over the last few years, the question of reasoning about aspect-oriented programs has been addressed by a number of authors. In this paper, we present a rely-guarantee approach to such reasoning. The rely-guarantee approach has proven extremely successful 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.
Khatchadourian, Raffi T. and Soundarajan, Neelam, "Rely-Guarantee Approach to Reasoning about Aspect-Oriented Programs" (2007). CUNY Academic Works.