JML

Question

におけるリターンで私はsize_ iはJMLでそれを行うことができますどのように

if(size_ == 0) 
    return null; 

に基づいて0の場合はnullを返すことが保証事後条件を設定する必要が声明場合は？何か案は？動作しない、次のとおりです。

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

    return size_.length() > 0; 
} 

あなたは、単にこのようにそれを書くことができます：：事前に

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

おかげ

Answer 1

は

が

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

例み

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

ここ

the documentation for \resultある：

3.2.14 \result
正常事後条件又は非ボイド方法の変形標的内の、特別な識別子\結果は、そのタイプのリターンである指定式でありますメソッドの型。このメソッドによって返された値を示します。 \ resultは、void以外のメソッドの宣言を変更するプラグマのensure、also_ensures、modifies、またはalso_modifiesプラグマ内でのみ許可されます。すべての

Answer 2

まず：size_、Objectまたはprimitive(int)でどのタイプ？

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

プリミティブ型をnullと比較することはできません。プリミティブ型が返されると考えられるnullを返すことはできません。我々はsize_がintであると仮定し、リターンがbooleanであれば、事後条件は

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