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

Question

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

例如，我有这样一个类：

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

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

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

Answer 1

可以，前提是被调用的方法不包含副作用并且声明为纯方法：

纯@/注释表明/@ ()是一个纯方法。纯方法是没有副作用的方法。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)
    { ... }
}