高级检索
    叶 俊, 谭庆平, 李 暾. 面向方面程序的属性推断[J]. 计算机研究与发展, 2013, 50(2): 344-351.
    引用本文: 叶 俊, 谭庆平, 李 暾. 面向方面程序的属性推断[J]. 计算机研究与发展, 2013, 50(2): 344-351.
    Ye Jun, Tan Qingping, Li Tun. The Property Inference of Aspect-Oriented Program[J]. Journal of Computer Research and Development, 2013, 50(2): 344-351.
    Citation: Ye Jun, Tan Qingping, Li Tun. The Property Inference of Aspect-Oriented Program[J]. Journal of Computer Research and Development, 2013, 50(2): 344-351.

    面向方面程序的属性推断

    The Property Inference of Aspect-Oriented Program

    • 摘要: 为简化面向方面程序(aspect-oriented programming,AOP)的形式化验证问题,Djoko等人对aspect进行了系统的分类,并确定了每类aspect能够保持的属性.分类之一的observer指一类对基程序的变量只读不写,且不修改其控制流的aspect,这类aspect能够保持所有的不包含Next算子的安全属性和活性属性.Djoko等人的工作可以避免针对织后程序的直接验证.在Djoko等人工作的基础上,提出了一种新的aspect分类——functor,并提出了属性推断的概念.functor是一种仅在特定条件下修改基程序性质的aspect.functor的确会造成基程序已有性质的失效,但却是以一种可预测的方式.属性推断就是根据基程序已有的性质和functor的特有性质,直接推断出织后程序的性质.functor同样避免了针对织后程序的直接验证,是对Djoko等人工作的重要补充.

       

      Abstract: 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.

       

    /

    返回文章
    返回