Aspects Preserving Properties

International audienceAspect 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