JML 后置条件包含类方法调用答案

【问题标题】：JML postcondition contains class method callJML 后置条件包含类方法调用
【发布时间】：2012-11-28 10:32:58
【问题描述】：

一个类方法的 JML 后置条件是否可以包含对另一个方法调用的调用

例如我有这个类：

public class A
{
    public int doA(x)
    { ... }

    public int doB(int x, int y)
    { ... }
}

对于doB的后置条件我可以有：ensures doA(x) = doA(y)？

【问题讨论】：

标签： java contracts jml post-conditions

【解决方案1】：

是的，只要被调用的方法不包含副作用并且被声明为纯方法：

/@pure @/ 注释表明 peek() 是一个纯方法。一种纯方法是一种没有副作用的方法。 JML 只允许断言使用纯方法。我们声明 peek() 是纯的，所以它可以用于 pop() 的后置条件。如果 JML 允许非纯方法在断言中，我们可能会无意中编写规范有副作用。这可能会导致编译时工作的代码启用了断言检查但在断言时不起作用检查被禁用。

http://www.ibm.com/developerworks/java/library/j-jml/index.html

public class A
{
    public /*@ pure @*/ int doA(int x)
    { ... }

    //@ requires ...
    //@ ensures doA(x) == doA(y)
    public int doB(int x, int y)
    { ... }
}

【讨论】：