java - JML で return を含む If ステートメント

Question

size_ が 0 の場合に null を返すことを保証する事後条件を設定する必要があります。

 if(size_ == 0)
  return null;

どうすればjmlでそれを行うことができますか? 何か案は？以下は機能しません：

//@ ensures size_ == null ==> \return true;

前もって感謝します

Answer 1

試す

//@ ensures size_ == null ==> \result == true;

例：

//@ ensures size_ == null ==> \result == true;
public boolean sizeUndefined() {
    if (size_ == null)
        return true;

    return size_.length() > 0;
}

次のように単純に記述することもできます。

//@ ensures size_ == null ==> \result;

のドキュメントは\result次のとおりです。

3.2.14 \result
通常の事後条件または非 void メソッドの変更ターゲット内では、特別な識別子 \result は、メソッドの戻り値の型を型とする仕様式です。メソッドによって返される値を示します。\result は、void 以外のメソッドの宣言を変更する、ensure、also_ensures、modifies、または also_modifies プラグマ内でのみ許可されます。

Answer 2

まず第一にsize_、 、Objectまたははどのような型primitive(int)ですか?

次に、メソッドの戻り値の型は何ですか? Objectまたはprimitive(boolean)？

プリミティブ型を と比較したり、プリミティブ型が返されるはずの場所にnull戻したりすることはできません。であるnullと仮定し、戻り値が である場合、事後条件は次のようになります。size_intboolean

//@ ensures size_ == 0 ==> \result;