Reasoning About Method Calls in Interface Specifications
Reasoning About Method Calls in Interface Specifications
复制标题
关于接口规范中方法调用的推理
DOI：
10.5381/jot.2006.5.5.a3
复制
发表时间：
2006
期刊：
影响因子：
--
通讯作者：
Peter Müller
中科院分区：
文献类型：
--
作者：
Ádám Darvas;Peter Müller
class Inconsistent { /*@ normal_behavior @ ensure\result == 0 && @ \result == 1; @*/ /*@ pure @*/ abstract int wrong（）; /*@ normal_behavior @ assignable \nothing; @ ensure\result == 6 + wrong（）& @ \result == 5 + wrong（）; @*/ int bar（）{ return 6; } }图6：错误的规范是不能满足的。用于验证在其规范中使用m的方法的理论。如果这一背景理论是不一致的，推理可能是不合理的。例如，上述公理是用于验证bar方法的背景理论的一部分，并且允许验证bar，尽管其规范显然不能满足。请注意，即使没有从bar的实现中调用wrong，也会出现这种不合理性。在实践中，不可满足的规范远没有方法错误的例子那么明显，因为它们通常涉及几个正常的行为规范案例，包括继承的规范。一个验证技术必须确保不能满足的规范不会导致不合理的推理。为了消除这种不合理的根源，我们使用比上述朴素公理化更弱的公理。这些公理要求人们通过给出一个证明，证明一个纯方法m的规范是可满足的，以便假设m和mS的性质。也就是说，m和mS的公理由以下前件保护：（r，OS ′ · specm（t，p，OS，r，OS ′））为了使用相应的公理，必须证明一个证明的存在。对于方法错误，不能给出一个证明r满足r = 0 <$r = 1。因此，相应公理的前件是假的，公理是无效的。接口规范中方法调用的合理性
class Inconsistent { /*@ normal_behavior @ ensures \result == 0 && @ \result == 1; @*/ /*@ pure @*/ abstract int wrong(); /*@ normal_behavior @ assignable \nothing; @ ensures \result == 6 + wrong() && @ \result == 5 + wrong(); @*/ int bar() { return 6; } } Figure 6: The specification of wrong is not satisfiable. theory used to verify methods that use m in their specification. If this background theory is inconsistent, the reasoning is potentially unsound. For instance, the above axiom is part of the background theory used to verify method bar and allows one to verify bar, although its specification is obviously not satisfiable. Note that this unsoundness occurs even though wrong is not called from bar’s implementation. In practice, unsatisfiable specifications are far less obvious than in the example of method wrong, because they typically involve several normal behavior specification cases including inherited specifications. A verification technique has to ensure that unsatisfiable specifications do not lead to unsound reasoning. To eliminate this source of unsoundness, we use axioms that are weaker than the naive axiomatization above. These axioms require one to prove, by giving a witness, that the specification of a pure method m is satisfiable in order to assume the properties of m and mS. That is, the axioms for m and mS are guarded by the following antecedent: (∃ r, OS ′ • specm(t, p, OS, r, OS ′) ) The existence of a witness has to be proven in order to employ the corresponding axiom. For method wrong, one cannot give a witness r that satisfies r = 0 ∧ r = 1. Therefore, the antecedent of the corresponding axiom is false, and the axiom is void. VOL 05, NO. 5 JOURNAL OF OBJECT TECHNOLOGY 75 REASONING ABOUT METHOD CALLS IN INTERFACE SPECIFICATIONS