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

Question

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

例如我有这个类:

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

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

对于 doB 的后置条件，我可以:确保 doA(x) = doA(y)？

Answer 1

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

The /@ pure @/ comment indicates that peek() is a pure method. A pure method is one that doesn't have side effects. JML only allows assertions to use pure methods. We declare peek() to be pure so it can be used in the postcondition of pop(). If JML allowed non-pure methods in assertions then we could inadvertently write specifications that had side effects. This could result in code that works when compiled with assertion checking enabled but doesn't work when assertion checking is disabled.

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