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