Skip to Main content Skip to Navigation
New interface
Reports (Research report)

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.
Document type :
Reports (Research report)
Complete list of metadata
Contributor : Pascal Fradet Connect in order to contact the contributor
Submitted on : Friday, January 22, 2010 - 6:19:47 PM
Last modification on : Thursday, October 27, 2022 - 4:02:42 AM
Long-term archiving on: : Thursday, June 17, 2010 - 11:13:54 PM


Files produced by the author(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⟩



Record views


Files downloads