java - 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

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

/ @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)
    { ... }
}