2

私はJavaでのコントラクトの意味についてもっと知りたいと思っています。

Javaでの2つのコントラクトの例を次に示します。

*/
* @pre  arr != null
* @pre  occurrences(4,arr) == occurrences(5, arr)
* @pre  arr[arr.length – 1] != 4
* @pre  forall 0 <= i < arr.length-2, arr[i] == 4 ==> arr[i+1] != 4
* @post forall 0 <= i < arr.length-1, $prev(arr[i]) == arr[i]
* @post $ret != arr
* @post permutation(arr, $ret)
* @post forall 0 <= i < arr.length-1, arr[i] == 4 ==> $ret[i] == 4
* @post forall 0 <= i < $ret.length-2, $ret[i] == 4 ==> $ret[i+1] == 5
/

そして2番目のもの：

*/
* @post (arr != null AND
*        occurrences(4,arr) == occurrences(5, arr) AND
*       arr[arr.length – 1] != 4 AND
*       forall 0 <= i < arr.length-2, arr[i] == 4 ==> arr[i+1] != 4)
<==        *
*       (forall 0 <= i < arr.length-1, $prev(arr[i]) == arr[i] AND
*        $ret != arr AND
*        permutation(arr, $ret) AND
*  $ret.length == arr.length AND
*        forall 0 <= i < arr.length-1, arr[i] == 4 ==> $ret[i] == 4 AND
*        forall 0 <= i < $ret.length-2, $ret[i]==4 ==> $ret[i+1] == 5)
/

ミッションは、これらの前提条件を使用して特定の配列を変更し、4が出現した後に5になるようにすることです。例：

fix45（{5,4,9,4,9,5}）-> {9,4,5,4,5,9}

fix45（{1,4,1,5}）-> {1,4,5,1}

これは私が書いたものです（それは動作します）：

public static  int pos (int[] arr, int k){

    while (arr[k]!=5){
        k=k+1;
        }
    return k;
}

public static  int[] fix45(int[] arr){
    int k=0;
    for(int i = 0; i<=arr.length-1; i++){
        if (arr[i] == 4){
            int place= pos(arr,k);
            arr[place]=arr[i+1];
            arr[i+1]=5;
            k=k+3;


        }

    }
    return arr;
}

私の質問：1。2つの契約の違いは何ですか？2.実際に前提条件を変更する必要がありますか？3.この「And」はどういう意味ですか？4. 2番目の契約に従ってコードをどのように変更する必要がありますか？

君たちありがとう。

4

2 に答える 2

4

1.2つの契約の違いは何ですか？

1つ目は、指定された前提条件を満たさなければならない方法で、パラメーターをメソッドに制限します。例として、arr引数はnullであってはなりません。そうでない場合はエラーになります。ただし、2番目の例では、任意の引数を渡すことができますが、引数が特定のレイアウト/構造である場合（nullではなく、同じ数の4と5を取得した場合、...）、配列を返す/変更する必要があります。結論に一致するそのような方法（私はの矢印を<== *回さなければならないと信じています）。

2.実際に前提条件を確認する必要があります

はい、特にあなたがそう言うなら。さらに、javadocコメントで言及する必要があり、そうでない場合に何が起こるかを示す必要があります。Javadocはそのための@throwsキーワードを取得しました。何かのようなもの

/**
 * (...)
 * @throws NullPointerException If the argument is <code>null</code>.
 * @throws IllegalArgumentException If the number of 4's and 5's is not the same.
 */

3.この「そして」はどういう意味ですか？

これANDは論理積です。true両方の引数/ステートメントがであるかどうかを評価しますtrue。

4.2番目の契約に従ってコードをどのように変更する必要がありますか？

仮説（の前の部分）と一致しない限り、配列をスローしたり、例外を設定したり、配列を変更したりしないでください==>。その場合、配列（および/または戻り値）は結論に従って変更する必要があります。

于 2011-03-30T21:01:28.263 に答える
2

私は知ることを主張することはできませんが、ここに与えられた条件の私の解釈があります。

まず第一に、あなたのコードは実際にはどちらの契約にも従わないようです。$ret != arrおよび条件に違反しforall 0 <= i < arr.length-1, $prev(arr[i]) == arr[i]ます。

  1. 両方の条件でarrを変更しない必要があるため（forall 0 <= i < arr.length-1, $prev(arr[i]) == arr[i]事後条件を介して、最初の条件（前と後）はすべて後の条件であるため、コントラクトは同じです。最初の条件では、前提条件が次の場合にエラーをスローする必要があります。 2つ目は、nullまたはその他の方法で無効な場合は、単に何か（または、またはその他の値など）を返す必要があることを意味しnullますarr。arr

  2. 前提条件に違反した場合は、おそらく違法な引数の例外をスローする必要があります（ただし、そのことについて契約を結んでいる人に相談する必要があります）。

  3. AND別々に記述されているかのように、論理的に条件を一緒に仮定します（ただし、OR柔軟性を高めるためにsと組み合わせて使用​​できます）

  4. する必要はありません。IllegalArgumentException前提条件が満たされていないときにをスローする代わりに、null

コメント用に編集：

戻り値がと同じものを$ret != arr参照できないことを意味すると思います。つまり、関数のどこかに新しいものを作成して、それを返す必要があります。int[]arrint[]

forall 0 <= i < arr.length-1, $prev(arr[i]) == arr[i]のすべての要素arr（何らかの理由で最後の要素を除く）は、以前（関数が呼び出される前）と同じでなければならないことを意味します。つまり、（多くの場合）それを変更することはできません。これは、まったく新しい配列を作成して返す必要があることと一致しています。

于 2011-03-30T20:53:31.250 に答える