面向方面程序的属性推断  

The Property Inference of Aspect-Oriented Program

作　　者：叶俊[1,2] 谭庆平[1] 李暾[1] 

机构地区：[1]国防科学技术大学计算机学院,长沙410073 [2]江南计算技术研究所,江苏无锡214083

出　　处：《计算机研究与发展》2013年第2期344-351,共8页Journal of Computer Research and Development

基　　金：国家自然科学基金项目(60773025)

摘　　要：为简化面向方面程序(aspect-oriented programming,AOP)的形式化验证问题,Djoko等人对aspect进行了系统的分类,并确定了每类aspect能够保持的属性.分类之一的observer指一类对基程序的变量只读不写,且不修改其控制流的aspect,这类aspect能够保持所有的不包含Next算子的安全属性和活性属性.Djoko等人的工作可以避免针对织后程序的直接验证.在Djoko等人工作的基础上,提出了一种新的aspect分类——functor,并提出了属性推断的概念.functor是一种仅在特定条件下修改基程序性质的aspect.functor的确会造成基程序已有性质的失效,但却是以一种可预测的方式.属性推断就是根据基程序已有的性质和functor的特有性质,直接推断出织后程序的性质.functor同样避免了针对织后程序的直接验证,是对Djoko等人工作的重要补充.To simplify the formal verification of programs developed with aspect-oriented programming （AOP） paradigm, Djoko et al. identified categories of aspects systematically and determined some class of properties that each aspect category can preserve. For example, one of the aspect categories named ＂observer ＂are those aspects that wouldn＇t modify the states and the control flow of their base program. The observer can preserve all safety and liveness properties that don＇t include ＂Next＂ operator. Their work can avoid direct verifications of the woven programs which always have larger scale than their base program. Their work is of great importance. Based on their work, this paper proposes a new aspect category named ＂functor＂ and proposes the concept of ＂property inference＂ （PI）. Functors are those aspects that add new functionalities to a base program under certain conditions. They have changed the property of a base program, but in an inferable way. PI infers the property of woven programs using the verified properties of a base program and special characterizes its aspects. PI also avoids direct verifications of the woven programs. Our work is an important supplement to Djoko＇s work.

关 键 词：面向方面程序 形式化验证 属性保持 属性推断 活性属性 安全属性 

分 类 号：TP311.1[自动化与计算机技术—计算机软件与理论]