Translucid contracts: Expressive specification and modular verification of aspect oriented interfaces

By: Mehdi Bagherzadeh

Download Paper

Abstract

As aspect-oriented (AO) programming techniques become more widely used, their use in critical systems such as aircraft and telephone networks, will become more widespread. However, careful reasoning about AO code seems difficult because: (1) advice may apply in too many places, and (2) standard specification techniques do not limit the control effects of advice. Commonly used black box specification techniques cannot easily specify control effects, such as advice that does not proceed to the advised code. In this work we avoid the first problem by using Ptolemy, a language with explicit event announcement. To solve the second problem we give a simple and understandable specification technique, 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 sound modular verification of typical interaction patterns used in AO code. We also show that translucid contracts allow interesting control effects to be specified and enforced.

ACM Reference

Bagherzadeh, M. 2011. Translucid contracts: Expressive specification and modular verification of aspect oriented interfaces. Iowa State University.

BibTeX Reference

@mastersthesis{bagherzadeh2011translucid-a,
  title = {Translucid contracts: Expressive specification and modular verification of aspect oriented interfaces},
  author = {Bagherzadeh, Mehdi},
  year = {2011},
  school = {Iowa State University},
  abstract = {
    As aspect-oriented (AO) programming techniques become more widely used, their
    use in critical systems such as aircraft and telephone networks, will become
    more widespread. However, careful reasoning about AO code seems difficult
    because: (1) advice may apply in too many places, and (2) standard
    specification techniques do not limit the control effects of advice. Commonly
    used black box specification techniques cannot easily specify control effects,
    such as advice that does not proceed to the advised code. In this work we
    avoid the first problem by using Ptolemy, a language with explicit event
    announcement. To solve the second problem we give a simple and understandable
    specification technique, 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 sound modular verification of typical interaction
    patterns used in AO code. We also show that translucid contracts allow
    interesting control effects to be specified and enforced.
  }
}