Постусловие 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)
    { ... }
}