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

是，所提供的称为方法不包括副作用和被声明为纯：

的/ @纯@ /注释指示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) 
    { ... } 
}