Open bisimulation for aspects

9 years 12 months ago
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 ...
Radha Jagadeesan, Corin Pitcher, James Riely
Added 12 Aug 2010
Updated 12 Aug 2010
Type Conference
Year 2007
Where AOSD
Authors Radha Jagadeesan, Corin Pitcher, James Riely
Comments (0)