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







Deposit Papers 


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

Full text available as:Adobe PDF

There is a later version of this eprint available: Click here to view it.


There is some consensus in the aspect-oriented community that a notion of interface between joinpoints and advice may be necessary for improved modularity of aspect-oriented programs, for modular reasoning, and for overcoming pointcut fragility. Different approaches for adding such interfaces, such as aspect-aware interfaces, pointcut interfaces, crosscutting interfaces, explicit joinpoints, quantified typed events, open modules and joinpoint types decouple aspects and base code, enhancing modularity. However, existing work has not shown how one can write specifications for such interfaces that will actually allow modular reasoning when aspects and base code evolve independently, and that are capable of specifying control effects, such as when advice does not proceed. The main contribution of this work is a specification technique that allows programmers to write modular specification of such interfaces and that allows one to reason about such control effects. We show that such specifications allow typical interaction patterns, and interesting control effects to be understood and enforced. We illustrate our techniques via an extension of Ptolemy, but we also show that our ideas can be applied in a straightforward manner to other notions of joinpoint interfaces, e.g. the crosscutting interfaces.

Keywords:Aspect-oriented programming, Modular reasoning, Modular verification, Interfaces, Design by contract
Subjects:Software: PROGRAMMING TECHNIQUES (E): Object-oriented Programming
Software: SOFTWARE ENGINEERING (K.6.3): Software/Program Verification (F.3.1)
Software: PROGRAMMING LANGUAGES: Language Constructs and Features (E.2)
ID code:00000633
Deposited by:Mehdi Bagherzadeh
Alternative Locations:

Available Versions of This Paper

Contact site administrator at: