AspectJML: Modular Specification and Runtime Checking for Crosscutting Contracts
				  by
	 Henrique Rebelo, Gary T. Leavens, Mehdi Bagherzadeh,
	  Hridesh Rajan, Ricardo Lima, Daniel M. Zimmerman,
		   Marcio Cornelio, and Thomas Thum

			       Abstract

Aspect-oriented programming (AOP) is a popular technique for
modularizing crosscutting concerns. In this context, researchers have
found that the realization of design by contract (DbC) is crosscutting
and fares better when modularized by AOP.  However, previous efforts
aimed at supporting crosscutting contracts modularly actually
compromised the main DbC principles. For example, in AspectJ-style,
reasoning about the correctness of a method call may require a
whole-program analysis to determine what advice applies and what that
advice does relative to DbC implementation and checking.  Also, when
contracts are separated from classes a programmer may not know about
them and may break them inadvertently.  In this paper we solve these
problems with AspectJML, a new specification language that supports
crosscutting contracts for Java code.  We also show how AspectJML
supports the main DbC principles of modular reasoning and contracts as
documentation.

Keywords: Design by contract, aspect-oriented programming,
crosscutting contracts, JML, AspectJ, AspectJML.

CR Categories: 
D.2.4 Software/Program Verification -- Programming by contract, Assertion Checkers; 
F.3.1 Specifying and Verifying and Reasoning about Programs -- Assertions, 
Invariant, Pre- and postconditions, Specification techniques.