Research On Open Temporal Logic Based Formal Verification And Modular Reasoning Of Aspect-Oriented Programs

AOP (aspect-oriented programming) is a new paradigm, which represents the promising trend of program paradigm. AOP reduces code refactoring due to the reconstruction of software projects, and improves the modularization and reusability of software systems. As a new program paradigm, the application and the research of aspect-oriented programming grows rapidly.Owing to the characteristics of quantification and obliviousness of aspect-oriented language, it is more likely to cause the problems of behavioral interference, and program verification and modular reasoning of aspect-oriented programs are more difficult than that of traditional paradigms. When the programmers implement some aspects, the interference between every aspect and the underlying system should be taken into account. Furthermore, when several aspects are woven into a same pointcut, possible dangerous interferences among different aspects should also be taken into account. The difficulty of program verification and modular reasoning of aspect-oriented programs highly blocks the development of aspect-oriented programming.Owing to mismatch between the semantic model of traditional formal logic and asymmetrical behavior of aspect-oriented programs, it is not fit for traditional formal logic to verify and modular reason aspect-oriented programs. Extended from traditional temporal logic, a new temporal logic named open temporal logic is proposed to verify and modular reason about aspect-oriented programs. The behavioral model of open temporal logic is asymmetrical and open. The major work and contributions are as follows:First, we define the syntax and semantics of open temporal logic. Open temporal logic introduces new path operators to specify internal parts and external parts, and introduces one new temporal operator to ensure some invariants during some external actions. The behavioral model of open temporal logic is an open system, which is asymmetrical and open, and is fit for specifying the behavioral model of aspect-oriented programs.Second, we propose to formally specify and verify aspect-oriented programs based on open temporal logic. Since there exist both similarity and difference between aspect interference and process interference of concurrent programs, we define crosscutable rely-condition to constrain possible crosscutting during the process of execution, which referenced from the method of specifying and verifying concurrent programs. Program specification of our research consists of three parts: pre-condition, crosscutable rely-condition and post-condition. We establish a proof system to formally verify aspect-oriented programs based on the program specifications. The soundness of the proof system is also proved.Third, we propose a method to modular constrain and modular reason about aspect-oriented programs. According to new characteristics of aspect-oriented programs, we define new modularization meaning of aspect-oriented programs. Similar to program specifications, module specifications consists of three conditions: pre-condition, crosscutable rely-condition and post-condition. Different modular constraints are defined by module specifications to support modular reasoning and modular composition of aspect-oriented programs. We introduce four modular constraints: crosscutable invariant, non-crosscutable invariant, crosscutable correct and non-crosscutable correct. Different modular constraints support different modular reliability.Fourth, we propose four kinds of crosscutting normal form. Based on the methods of formal verification and modular reasoning of this research, we settle the behavioral problems that different aspects woven to a same pointcut will interfere with each other. Based on different modular constraints and compositional constraints of aspects, crosscutting normal forms ensure that different aspects woven to a same pointcut will not interfere with each other. We introduce four kinds of crosscutting normal form: crosscutting invariant normal form, non-crosscutting invariant normal form, crosscutting correct normal form and non-crosscutting correct normal form.