Aspects Preserving Properties

Simplice Djoko Djoko 1, 2 Rémi Douence 3 Pascal Fradet 1
1 POP ART - Programming languages, Operating Systems, Parallelism, and Aspects for Real-Time
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
3 ASCOLA - Aspect and composition languages
LINA - Laboratoire d'Informatique de Nantes Atlantique, Département informatique - EMN, Inria Rennes – Bretagne Atlantique
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 can be 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 and confiners. 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. % These categories (along with three other) are defined precisely 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 \wrt a common imperative base language. Each category and language are illustrated by simple examples. The appendix provides semantics and examples 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 :
[Research Report] RR-7155, INRIA. 2009
Liste complète des métadonnées
Contributeur : Pascal Fradet <>
Soumis le : vendredi 22 janvier 2010 - 18:19:47
Dernière modification le : vendredi 12 octobre 2018 - 01:19:10
Document(s) archivé(s) le : jeudi 17 juin 2010 - 23:13:54


Fichiers produits par l'(les) auteur(s)


  • HAL Id : inria-00449851, version 1


Simplice Djoko Djoko, Rémi Douence, Pascal Fradet. Aspects Preserving Properties. [Research Report] RR-7155, INRIA. 2009. 〈inria-00449851〉



Consultations de la notice


Téléchargements de fichiers