AspectJML: Modular Specfication and Runtime Checking for Crosscutting Contracts

PDF Download Download Paper


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

Bib Info

  author = {Henrique Rebelo and Gary T. Leavens and Mehdi Bagherzadeh and Hridesh Rajan and Ricardo Massa Lima and Daniel Zimmerman and Marcio Cornelio and Thumas Thum},
  title = {AspectJML: Modular Specfication and Runtime Checking for Crosscutting Contracts},
  booktitle = {Proceedings of the 13th International Conference on Aspect-Oriented Software Development},
  series = {AOSD},
  year = {2014},
  location = {Lugano, Switzerland},