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