26

私は Code Contracts で不変条件を実証しようとしています。文字列の並べ替えられたリストの例を挙げたいと思いました。配列を内部的に維持し、追加などのための予備スペースを備えています-List<T>基本的には と同じです。アイテムを追加する必要がある場合は、それを配列に挿入するなどします。3 つの不変条件があると考えました。

  • カウントは適切である必要があります: 非負であり、最大でバッファ サイズと同じ大きさです。
  • バッファの未使用部分はすべて null にする必要があります
  • バッファの使用部分の各アイテムは、少なくともその前のアイテムと同じくらい「大きい」必要があります

今、私はこの方法でそれを実装しようとしました:

[ContractInvariantMethod]
private void ObjectInvariant()
{
    Contract.Invariant(count >= 0 && count <= buffer.Length);
    for (int i = count; i < buffer.Length; i++)
    {
        Contract.Invariant(buffer[i] == null);
    }
    for (int i = 1; i < count; i++)
    {
        Contract.Invariant(string.Compare(buffer[i], buffer[i - 1]) >= 0);
    }
}

残念ながら、ccrewriteループを台無しにしています。

ユーザー ドキュメントによると、このメソッドは への一連の呼び出しである必要がありますContract.Invariant。本当にこのようなコードを書き直す必要がありますか?

Contract.Invariant(count >= 0 && count <= buffer.Length);
Contract.Invariant(Contract.ForAll
    (count, buffer.Length, i => buffer[i] == null));
Contract.Invariant(Contract.ForAll
    (1, count, i => string.Compare(buffer[i], buffer[i - 1]) >= 0));

それは機能しますが、やや醜いです。（以前の試みよりもはるかに優れています。念のため。）

私の期待は不合理ですか？私の不変条件は不合理ですか？

(コード コントラクト フォーラムでも質問されています。関連する回答があれば、ここに追加します。)

4

3 に答える 3

8

(予備の) MSDN ページから、Contract.ForAll メンバーが 2 つの範囲コントラクトを支援できるようです。ただし、ドキュメントはその機能についてあまり明示的ではありません。

//untested
Contract.Invariant(Contract.ForAll(count, buffer.Length, i => buffer[i] == null));
Contract.Invariant(Contract.ForAll(1, count, 
    i => string.Compare(buffer[i], buffer[i - 1]) >= 0));
于 2009-07-30T20:57:18.693 に答える
3

（ヘンクの答えを受け入れるつもりですが、これを追加する価値があると思います。）

質問はMSDNフォーラムで回答されましたが、結果として、最初のフォームは機能しないと予想されます。不変条件は、実際には、への一連の呼び出しである必要がありContract.Invariant、それだけです。

これにより、静的チェッカーが不変条件を理解して強制することがより実現可能になります。

この制限は、すべてのロジックを別のメンバー（IsValidプロパティなど）に配置し、次のコマンドを呼び出すだけで回避できます。

Contract.Invariant(IsValid);

それは間違いなく静的チェッカーを台無しにするでしょうが、場合によってはそれが有用な代替手段になるかもしれません。

于 2009-07-31T06:29:09.887 に答える
1

デザイナーは車輪を少し再発明していませんか?

古き良きものの何が問題だったのか

bool Invariant() const; // in C++, mimicking Eiffel

?

C# には const がありませんが、なぜInvariant関数を定義できないのでしょうか。

private bool Invariant()
{
  // All the logic, function returns true if object is valid i.e. function
  // simply will never return false, in the absence of a bug
}
// Good old invariant in C#, no special attributes, just a function

そして、その機能に関してコード契約を使用するだけですか?

[ContractInvariantMethod]
private void ObjectInvariant()
{
    Contract.Invariant(Invariant() == true);
}

ナンセンスなことを書いているのかもしれません。

于 2009-08-23T22:36:38.770 に答える