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

By: Mehdi Bagherzadeh, Hridesh Rajan, Gary T. Leavens, and Sean 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. AOSD ’11: 10th International Conference on Aspect-Oriented Software Development (Mar. 2011).

BibTeX Reference

@inproceedings{bagherzadeh2011translucid-b,
  author = {Mehdi Bagherzadeh and Hridesh Rajan and Gary T. Leavens and Sean Mooney},
  title = {Translucid Contracts: Expressive Specification and Modular Verification for Aspect-Oriented Interfaces},
  booktitle = {AOSD '11: 10th International Conference on Aspect-Oriented Software Development},
  location = {Porto de Galinhas, Brazil},
  month = {March},
  year = {2011},
  entrysubtype = {conference},
  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.
  }
}