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







Deposit Papers 


Bagherzadeh, Mehdi, Rajan, Hridesh, Gary T., Leavens and Mooney, Sean (2010) Translucid Contracts: Expressive Specification and Modular Verification for Aspect-Oriented Interfaces. Technical Report 10-02a, Department of Computer Science, Iowa State University.

Full text available as:Adobe PDF

This is the latest version of this eprint.


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.

Keywords:Aspect-oriented programming, Modular reasoning, Modular verification, Interfaces, Design by contract
Subjects:Software: GENERAL
ID code:00000648
Deposited by:Mehdi Bagherzadeh on 14 July 2010

Available Versions of This Paper

Contact site administrator at: