Modularizing crosscutting contracts with AspectJML

It is claimed in the literature that the contracts of a system present crosscutting structure during its realization. In this context, there has been attempts to improve separation of crosscutting contracts, e.g. by aspect-oriented programming and design by contract languages, but none give programmers textual separation of contracts/specifications and modular reasoning at the same time. In this demonstration we show how our language, AspectJML, a simple and practical aspect-oriented extension to JML, allows the separation of crosscutting contracts while maintaining the key benefits of a design by contract language, like documentation and modular reasoning. AspectJML's quantified statements, written in terms of AspectJ pointcut language, allow one to select join points in which the contracts are written in a modular and convenient way. Also, all the crosscutting contracts are well documented in the class they apply to, thus allowing the reasoning about crosscutting contracts in a modular fashion. This demonstration will proceed by discussing several examples that highlights the main features of the AspectJML language and show the use of AspectJML's compiler, ajmlc. We will conclude with a discussion of ongoing work on design, implementation and runtime checking of both Java and AspectJ programs with AspectJML/ajmlc.