JML postcondition contains class method call

Question

Can a JML postcondition for a class method contain a call to another method call

For example I have this class:

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

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

For the postcondition of doB can I have: ensures doA(x) = doA(y)?

Answer 1

Yes, provided the called method doesn't include side effects and is declared as pure:

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