S. Djoko Djoko, R. Douence, P. Fradet. Aspects Preserving Properties. In Proc. of the ACM SIGPLAN 2008 Symposium on Partial Evaluation and Program Manipulation (PEPM'08), Pages 135-145, January 2008.
Aspect Oriented Programming can arbitrarily distort the semantics of programs. In particular, weaving can invalidate crucial safety and liveness properties of the base program. In this article, we identify categories of aspects that preserve some classes of properties. It is then sufficient to check that an aspect belong to a specific category to know which properties will remain satisfied by woven programs. % Our categories of aspects, inspired by Katz's, comprise observers, aborters and confiners. Observers do not modify the base program's state and control-flow. Aborters are observers which may also abort executions. Confiners only ensure that executions remain in the reachable states of the base program. % These categories are defined precisely based on a language independent abstract semantics framework. The classes of properties are defined as subsets of LTL for deterministic programs and CTL* for non-deterministic ones. We can formally prove that, for any program, the weaving of any aspect in a category preserves any property in the related class. We give examples to illustrate each category and provide the proof of preservation for one category in the appendix
[ Aspect-oriented programming ] [ Weaving ] [ Semantics ] [ Temporal properties ] [ Proofs ]
Pascal Fradet http://pop-art.inrialpes.fr/people/fradet/
@InProceedings{PEPM08,
Author = {Djoko Djoko, S. and Douence, R. and Fradet, P.},
Title = {Aspects Preserving Properties},
BookTitle = {Proc. of the ACM SIGPLAN 2008 Symposium on Partial Evaluation and Program Manipulation (PEPM'08)},
Pages = {135--145},
Publisher = {ACM},
Month = {January},
Year = {2008}
}
Get EndNote Reference (.ref)