面向方面软件重构等价性形式化证明方法

软件重构在不改变程序行为的情况下通过对代码进行小的改进以提升设计，使之更容易理解和维护，面向方面的程序设计是软件开发的新技术，为了有效实施面向方面的软件重构，需要开发者识别面向方面程序的转化规则。然而，由于使用的AOP语言没有形式化的语义定义，难以确认转化和重构的程序运行行为。本文对MCI操作语义的面向方面的扩展使之支持程序的方面特征的描述，定义了两个程序的观测等价，讨论了AspectJ的形式语义模型的建立，在MCI的语义下形式化地精确证明了Add Before-executing编程规则的观测等价性，其基本原理和方法可以适用于其他规则的证明，通过上述工作提出了面向方面重构的程序和它的面向对象程序原型等价性的证明方法。

An Equivalence Proving in Formal Method for Aspect-Oriented Refactory

Refactoring is that you make small changes to your code to improve your design,making it easier to understand and maintrained without to change program behaviours.Aspect Oriented Programming(AOP)is a new technology for software development.In order to explore the benefits of refactoring aspect-oriented developers are identifying common transformations for aspect-oriented programs the laws proof.However,they lack support for assuring that the transformations observation behaviour and are indeed refactorings because there is not formal semantics in the AOP language that we have used.In this paper,an operational semantics for Method Call Interception(MCI)is extented to fit in with represent AOP featurs.An equivalence relation stating that two programs have the same observation behaviour is defined;the paper presents a formal model for the semantics of AspectJ.We use these concepts and discuss exactness for its laws in formal mothed MCI.The observation equivalence proving of Add Before-executing law can be used in other law.In conclusion,we show how it is possible to prove that an new aspect-oriented program by refactoring is equivalent its Object Oriented prototype