1

コード コントラクトを含む次のコードでいくつかの警告が表示されます。

public static int Min(IEnumerable<int> set)
{
    Contract.Requires(set != null);
    Contract.Requires(set.Any());

    Contract.Ensures(Contract.ForAll(set, x => x >= Contract.Result<int>()));

    int min = set.Min();

    return min;
}

static void Main(string[] args)
{
    Console.WriteLine(Min(new int[] {3,4,5}));
    Console.WriteLine(Min(new int[] {})); // should fail
}

次の警告が表示されます。

Requires unproven: set.Any() on Min(new int[] {3,4,5})

Ensures unproven: Contract.ForAll(set, x => x > Contract.Result<int>())

2 つの質問:

  1. 私の事後条件には x >= Contract.Result() と記載されていますが、「証明されていないことを保証する」という警告には x > Contract.Result() と記載されています。(Greater or equal vs. Greater) これはどうして起こるのでしょうか?

  2. 上記のステートメントで set.Any() を証明できないのはなぜですか?

前もって感謝します。

4

2 に答える 2

1

このEnsures句は、最初からすべての に対して有効ではありませんIEnumerable。IEnumerable最初に列挙されたときに 1 つのシーケンスを返し (例: 1, 2, 3)、2 回目に別のリストを返す (例: ) を書くことができます0。これは、任意の実装を持つインターフェイスです。

IEnumerableには通常、多くの (生成される可能性のある) 処理が隠されています。具体的な実行時型が何らかの形でわかっていたとしても、CC がそれを見抜くことはできないと思います。

CC は についてヒューリスティックに推論することさえできIEnumerableますか? それは私にとって新しいことです。複数回列挙された場合、シーケンスは変更されないと仮定する必要があります (データベースクエリの場合、これは自明に誤りです)。

主観的な補足として、CC チェッカーがあまりにも限定的すぎて役に立たないことがわかったことを指摘しておきます。興味深い特性を証明するために、非常に多くの問題が発生します。抽象化にうまく対応できません。

于 2012-12-12T12:22:29.313 に答える
0

STATIC コード チェッカーが、セットにデータが含まれているかどうかを判断する方法はありません。考えてみると、チェッカーは、メソッド自体の内部でいくつかのコントラクトが定義されていない限り、さまざまなメソッドとプロパティが何をするかを知りません。

あなたの場合、チェッカーは、拡張メソッド Any() または Min() の結果が何であるかを知らないため、Requires と Ensures を検証できません。

パラメーターの型を変更することで警告の数を減らすことができますが、コード チェッカーはコードが Min(...) の要件を満たしていることを確認できません。

タイプを int[] または List に変更すると、一部の警告が消える場合があります。次のコードは警告を返しません。

    public static int Min(List<int> set)
    {
        Contract.Requires(set != null);
        Contract.Requires(set.Count>0);


        Contract.Ensures(Contract.ForAll(set, x => x >= Contract.Result<int>()));

        int min = set.Min();

        return min;
    }

    static void Main(string[] args)
    {

        Console.WriteLine(Min(new List<int> { })); // should fail
        Console.WriteLine(Min(new List<int> { 3, 4, 5 }));
        Console.ReadKey();
    }

もちろん、このコードを実行すると例外が発生して失敗するため、おそらくコード チェッカーはこれを検出するのに十分なほどスマートです。

元の順序を維持すると、警告が表示されます。

        Console.WriteLine(Min(new List<int> { 3, 4, 5 }));
        Console.WriteLine(Min(new List<int> { })); // should fail

どちらの場合も、Main() に Contract.Ensures(false) を追加するなど、クレイジーな提案も得られます。

于 2012-12-12T12:47:47.597 に答える