Aspects Preserving Properties

Simplice Djoko Djoko 1, 2, 3 Rémi Douence 1 Pascal Fradet 3
1 ASCOLA - Aspect and composition languages
Inria Rennes – Bretagne Atlantique , Département informatique - EMN, LINA - Laboratoire d'Informatique de Nantes Atlantique
3 POP ART - Programming languages, Operating Systems, Parallelism, and Aspects for Real-Time
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
Abstract : 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. Specialized aspect languages are then designed to ensure that aspects belong to a specific category and, therefore, that woven programs will preserve the corresponding properties. Our categories of aspects, inspired by Katz's, comprise observers, aborters, confiners and weak intruders. Observers introduce new instructions and a new local state but they 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. Weak intruders are confiners between two advice executions. These categories (along with two others) are defined formally based on a language independent abstract semantics framework. The classes of preserved 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 present, for most aspect categories, a specialized aspect language which ensures that any aspect written in that language belongs to the corresponding category. It can be proved that these languages preserve the corresponding classes of properties by construction. The aspect languages share the same expressive pointcut language and are designed w.r.t. a common imperative base language. Each category and language is illustrated by simple examples. The appendix provides se- mantics and two instances of proofs: the proof of preservation of properties by a category and the proof that all aspects written in a language belong to the corresponding category.
Type de document :
Article dans une revue
Science of Computer Programming, Elsevier, 2011, 77 (3), pp.393-422. 〈10.1016/j.scico.2011.10.010〉
Liste complète des métadonnées

https://hal.inria.fr/inria-00638852
Contributeur : Rémi Douence <>
Soumis le : lundi 7 novembre 2011 - 14:51:51
Dernière modification le : vendredi 22 juin 2018 - 09:34:39

Lien texte intégral

Identifiants

Citation

Simplice Djoko Djoko, Rémi Douence, Pascal Fradet. Aspects Preserving Properties. Science of Computer Programming, Elsevier, 2011, 77 (3), pp.393-422. 〈10.1016/j.scico.2011.10.010〉. 〈inria-00638852〉

Partager

Métriques

Consultations de la notice

376