The Property Inference of Aspect-Oriented Program

To simplify the formal verification of programs developed with aspect-oriented programming (AOP) paradigm, Djoko et al. identified categories of aspects systematically and determined some class of properties that each aspect category can preserve. For example, one of the aspect categories named “observer ”are those aspects that wouldn’t modify the states and the control flow of their base program. The observer can preserve all safety and liveness properties that don’t include “Next” operator. Their work can avoid direct verifications of the woven programs which always have larger scale than their base program. Their work is of great importance. Based on their work, this paper proposes a new aspect category named “functor” and proposes the concept of “property inference” (PI). Functors are those aspects that add new functionalities to a base program under certain conditions. They have changed the property of a base program, but in an inferable way. PI infers the property of woven programs using the verified properties of a base program and special characterizes its aspects. PI also avoids direct verifications of the woven programs. Our work is an important supplement to Djoko’s work.