Crosscutting Invasion and Crosscutting Invariant

Owing to the characteristics of quantification and obliviousness of aspect-oriented language, modular behavioral analysis and modular reasoning are more difficult than that of the traditional paradigms. To deal with crosscutting safety and crosscutting quality in aspect-oriented language, crosscutting modules and affected modules are constrained with pre-conditions and post-conditions, but assigning blame for pre-condition and post-condition failures during the process of crosscutting poses subtle and complex problems. To analyze behavioral effect of a crosscutting concern, the programmer should consider the aspect itself and the part of the system it affects. Furthermore, when several aspects are woven at a same pointcut, the analysis of possible dangerous interferences becomes more complex. Similar to the notion of behavioral subtyping in object-oriented language, a notion of crosscutting invariant is proposed. In order to check the behavioral errors of violating crosscutting invariability and four other simple behavioral errors, an algorithm based on software behavioral contracts is proposed. To formalize this algorithm, crosscutting contract calculus and a set of contract elaboration rules are presented. The contract soundness theorem which ensures the correctness of the contract elaboration process is stated and proved. An example is also represented to show how to use these contract elaboration rules to check and analyze the behavioral errors.