Specialized Aspect Languages Preserving Classes of Properties

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 previous work, we have identified categories of aspects that preserve classes of temporal properties. We have formally proved that, for any program,the weaving of any aspect in a category preserves all properties in the related class. In this article, after a summary of our previous work,we present, for each aspect category, 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 point cut language and are designed w.r.t. a common imperative base language. Each language is illustrated by simple examples. We also prove that all aspects written in one of the languages belong to the corresponding category.