AspectJML: Modular Specfication and Runtime Checking for Crosscutting Contracts

By: Henrique Rebelo, Gary T. Leavens, Mehdi Bagherzadeh, Hridesh Rajan, Ricardo Massa Lima, Daniel Zimmerman, Marcio Cornelio, and Thumas Thum

Abstract

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.

ACM Reference

Rebelo, H. et al. 2014. AspectJML: Modular Specfication and Runtime Checking for Crosscutting Contracts. Proceedings of the 13th International Conference on Aspect-Oriented Software Development (2014).

BibTeX Reference

@inproceedings{rebelo2014aspectjml,
  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},
  entrysubtype = {conference},
  abstract = {
    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.
  }
}