2

トーナメントでラウンドを実行するアプリケーションがあり、この単純化されたコード構造に関する契約警告が表示されます。

    public static void LoadState(IList<Object> stuff)
    {
        for(int i = 0; i < stuff.Count; i++)
        {
            // Contract.Assert(i < stuff.Count);
            // Contract.Assume(i < stuff.Count);

            Object thing = stuff[i];

            Console.WriteLine(thing.ToString());
        }
    }

警告は次のとおりです。

contracts: requires unproven: index < @this.Count

私は何が間違っているのですか？どうすればこれを証明できIList<T>ますか？これは静的アナライザのバグですか？バグレポートをMicrosoftに送信するにはどうすればよいですか？

4

2 に答える 2

3

それは奇妙に見えます。残念ながら、コードコントラクトを備えたVS2010のProバージョンを使用しているため、cccheck自分で遊んでみることができません。

foreachループを使用するだけでなく、インデックスが絶対に必要ですか？

念のために言っておきますが、上記の簡略化した例でも同じエラーが発生しますか？単純化によって問題が解決されていないことを常に確認する価値があります:)たとえばstuff、契約チェッカーが保証を無効にするために使用する可能性のある他のことをしstuff.Countますか？

于 2009-08-04T21:59:37.517 に答える
1

コード コントラクトのバージョン 1.2.21023.14 でこれを確認しましたが、警告は表示されませんでした。私の推測では、それはその後修正されたバグです。

于 2009-10-31T18:04:25.793 に答える