オブジェクト不変式のコードでどのくらい自由になれますか？

Question

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

• カウントは賢明でなければなりません：負ではなく、最大でバッファサイズと同じです
• バッファの未使用部分のすべてがnullである必要があります
• バッファの使用済み部分の各アイテムは、少なくとも<！> quot; big <！> quot;でなければなりません。前のアイテムとして

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

[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));

それは機能しますが、ややいです。 （それは私の以前の試みよりもはるかに良いです、あなたに気をつけてください。）

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

（ Code Contractsフォーラムの質問。関連する回答はここに追加します。）

Answer 1

（予備の）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));

Answer 2

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

質問は MSDNフォーラム、そして結果は、最初のフォームが機能するとは思われません 。不変条件は、本当に、一連のContract.Invariantの呼び出しである必要があり、それだけです。

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

この制限は、すべてのロジックを別のメンバーに置くだけで回避できます。 IsValidプロパティ、および呼び出し：

Contract.Invariant(IsValid);

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

Answer 3

デザイナーは車輪を再発明しませんか？

古き良き

の問題点

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);
}

たぶん私はナンセンスを書いていますが、その場合でも、誰もが間違ったことを言うと、教訓的な価値があります。