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

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