AspectJML: Modular Specification and Runtime Checking for Crosscutting Contracts

By: Henrique Rebêlo, Gary T. Leavens, Mehdi Bagherzadeh, Hridesh Rajan, Ricardo Massa Ferreira Lima, Daniel M. Zimmerman, Márcio Cornélio, and Thomas Thüm

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

Rebêlo, H. et al. 2014. AspectJML: Modular Specification and Runtime Checking for Crosscutting Contracts. 13th International Conference on Modularity, MODULARITY, Lugano, Switzerland (2014), 157–168.

BibTeX Reference

@inproceedings{RebeloETAL2014,
  author = {Henrique Reb{\^{e}}lo and Gary T. Leavens and Mehdi Bagherzadeh and Hridesh Rajan and Ricardo Massa Ferreira Lima and Daniel M. Zimmerman and M{\'{a}}rcio Corn{\'{e}}lio and Thomas Th{\"{u}}m},
  title = {AspectJML: Modular Specification and Runtime Checking for Crosscutting Contracts},
  booktitle = {13th International Conference on Modularity, MODULARITY, Lugano, Switzerland},
  pages = {157--168},
  year = {2014},
  publisher = {{ACM}},
  editor = {Walter Binder and Erik Ernst and Achille Peternier and Robert Hirschfeld},
  doi = {10.1145/2577080.2577084},
  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.},
}