java - 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 として宣言されている場合:

/ @ pure @ / コメントは、peek() が純粋なメソッドであることを示しています。純粋なメソッドとは、副作用のないメソッドです。JML では、アサーションで純粋なメソッドを使用することのみが許可されます。pop() の後置条件で使用できるように、peek() を純粋であると宣言します。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)
    { ... }
}