Verifying Aspect-Oriented Programs Using Open Temporal Logic

The behavior model of traditional temporal logic is closed and symmetrical, while the behavior model of aspect-oriented programs is open and asymmetrical. When the programmer designs the base-code, he is not sure what aspects will be woven to it. It is indirect and difficult to specify and verify the behavior of aspect-oriented programs by using traditional temporal logic. In this paper, we propose a new temporal logic named open temporal logic, which introduced some new path operators and one new temporal operator. Since paths are divided into two kinds: internal parts and external parts, the behavioral model of open temporal logic is open and asymmetrical. Base on open temporal logic and the proof system of traditional rely-guarantee method, a new proof system is given to verify the behavior of aspect-oriented programs.