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

Date
2010-07-01
Authors
Bagherzadeh, Mehdi
Rajan, Hridesh
Rajan, Hridesh
Leavens, Gary
Mooney, Sean
Journal Title
Journal ISSN
Volume Title
Publisher
Source URI
Altmetrics
Authors
Research Projects
Organizational Units
Computer Science
Organizational Unit
Journal Issue
Series
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.

Description
<p>Copyright © 2010, Mehdi Bagherzadeh, Hridesh Rajan, Gary T. Leavens and Sean Mooney. Submitted for publication.</p>
Keywords
Aspect-oriented programming, Modular reasoning, Modular verification, Interfaces, Design by contract
Citation
Collections