Open bisimulation for aspects

We define and study bisimulation for proving contextual equivalence in an aspect extension of the untyped lambda-calculus. To our knowledge, this is the first study of coinductive reasoning principles aimed at proving equality of aspect programs. The language we study is very small, yet powerful enough to encode mutable references and a range of temporal pointcuts (including cflow and regular event patterns). Examples suggest that our bisimulation principle is useful. For an encoding of higher-order programs with state, our methods suffice to establish well-known and well-studied subtle examples involving higher-order functions with state. Even in the presence of first class dynamic advice and expressive pointcuts, our reasoning principles show that aspect-aware interfaces can aid in ensuring that clients of a component are unaffected by changes to an implementation. Our paper generalizes existing results given for open modules to also include a variety of history-sensitive pointcuts ...

• Type: Conference
• Year: 2007
• Where: AOSD
• Authors: Radha Jagadeesan, Corin Pitcher, James Riely
• Keywords: AOSD 2007, Contextual Equivalence, Reasoning Principles, Regular Event Patterns, Software Engineering