Translucid Contracts: Expressive Specification and Modular Verification for Aspect-Oriented Interfaces

By: Mehdi Bagherzadeh, Hridesh Rajan, Gary T. Leavens, and Sean L. Mooney

Abstract

As aspect-oriented programming techniques become more widely used, their use in critical systems, including safety-critical systems such as aircraft and mission-critical systems such as telephone networks, will become more widespread. However, careful reasoning about aspect-oriented code seems difficult with standard specification techniques. The difficulty stems from the difficulty of understanding control effects, such as advice that does not proceed to the original join point, because most common specification techniques do not make it convenient to specify such control effects. In this work we give a simple and understandable specification technique, which we call translucid contracts, that not only allows programmers to write modular specifications for advice and advised code, but also allows them to reason about the code’s control effects. We show that translucid contracts support modular verification of typical interaction patterns used in aspect-oriented code. We also show that translucid contracts allow interesting control effects to be understood and enforced. Our proposed specification and verification approach is proved sound.

ACM Reference

Bagherzadeh, M. et al. 2011. Translucid Contracts: Expressive Specification and Modular Verification for Aspect-Oriented Interfaces. Proceedings of the 10th International Conference on Aspect-Oriented Software Development, AOSD, Porto de Galinhas, Brazil (2011), 141–152.

BibTeX Reference

@inproceedings{BagherzadehRajanLeavensMooney2011,
  author = {Mehdi Bagherzadeh and Hridesh Rajan and Gary T. Leavens and Sean L. Mooney},
  title = {Translucid Contracts: Expressive Specification and Modular Verification for Aspect-Oriented Interfaces},
  booktitle = {Proceedings of the 10th International Conference on Aspect-Oriented Software Development, AOSD, Porto de Galinhas, Brazil},
  pages = {141--152},
  year = {2011},
  publisher = {{ACM}},
  editor = {Paulo Borba and Shigeru Chiba},
  doi = {10.1145/1960275.1960293},
  abstract = {
  As aspect-oriented programming techniques become more widely used, their use
  in critical systems, including safety-critical systems such as aircraft and
  mission-critical systems such as telephone networks, will become more
  widespread. However, careful reasoning about aspect-oriented code seems
  difficult with standard specification techniques. The difficulty stems from
  the difficulty of understanding control effects, such as advice that does not
  proceed to the original join point, because most common specification
  techniques do not make it convenient to specify such control effects. In this
  work we give a simple and understandable specification technique, which we
  call translucid contracts, that not only allows programmers to write modular
  specifications for advice and advised code, but also allows them to reason
  about the code's control effects. We show that translucid contracts support
  modular verification of typical interaction patterns used in aspect-oriented
  code. We also show that translucid contracts allow interesting control effects
  to be understood and enforced. Our proposed specification and verification
  approach is proved sound.},
}