Laboratory for Software Design

Got a question?

Got a question or comment? Contact us at (515) 294-6168 or hridesh@iastate.edu.

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

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.

Bibliographic Information

@inproceedings{Bagherzadeh-Rajan-Leavens-Mooney-10,
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},
}

Most recent version: [PDF] [Slides]