Notice

The website of Tom Schrijvers has moved to http://people.cs.kuleuven.be/~tom.schrijvers. Please adjust any links you maintain as this copy will be taken down shortly.


Compositional Reasoning About Aspect Interference


Ismael Figueroa, Tom Schrijvers, Nicolas Tabareau, Eric Tanter.
Modularity 2014.
2014.

Abstract

Oliveira and colleagues recently developed a powerful model to reason about mixin-based composition of effectful components and their interference, exploiting a wide variety of techniques such as equational reasoning, parametricity, and algebraic laws about monadic effects. This work addresses the issue of reasoning about interference with effectful aspects in the presence of unrestricted quantification through pointcuts. While global reasoning is required, we show that it is possible to reason in a compositional manner, which is key for the scalability of the approach in the face of large and evolving systems. We establish a general equivalence theorem that is based on a few conditions that can be established, reused, and adapted separately as the system evolves. Interestingly, one of these conditions, local harmlessness, can be proven by a translation to the mixin setting, making it possible to directly exploit previously established results about certain kinds of harmless extensions.

BibTeX

@inproceedings{modularity2014,
  title = {Compositional Reasoning About Aspect Interference},
  author = {Ismael Figueroa, Tom Schrijvers, Nicolas Tabareau, Eric Tanter},
  year = {2014},
  booktitle = {Modularity 2014},
  url = {/Research/papers/modularity2014.pdf},
  abstract = {Oliveira and colleagues recently developed a powerful model to
  reason about mixin-based composition of effectful components and
  their interference, exploiting a wide variety of techniques such as
  equational reasoning, parametricity, and algebraic laws about
  monadic effects. This work addresses the issue of reasoning about
  interference with effectful aspects in the presence of unrestricted
  quantification through pointcuts. While global reasoning is
  required, we show that it is possible to reason in a compositional
  manner, which is key for the scalability of the approach in the face
  of large and evolving systems. We establish a general equivalence
  theorem that is based on a few conditions that can be
  established, reused, and adapted separately as the system
  evolves. Interestingly, one of these conditions, local
  harmlessness, can be proven by a translation to the mixin setting,
  making it possible to directly exploit previously established results about
  certain kinds of harmless extensions.
  },
}