この契約を証明するには何が必要ですか？必要ですか？

私はトーナメントでのラウンドを通じて実行するアプリケーションを持っている、と私は、この単純化されたコードの構造上の契約の警告を取得しています：私は何をやっているこの契約を証明するには何が必要ですか？必要ですか？

contracts: requires unproven: index < @this.Count

：

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

警告があります違う？ IList<T>でこれをどのように証明できますか？これはスタティックアナライザのバグですか？バグレポートをMicrosoftに提出するにはどうすればよいですか？

出典

2009-08-04 John Gietzen

バージョン契約の1.2.21023.14でこれをチェックし、警告が表示されませんでした。私の推測では、これは修正されているバグだということです。

出典

2009-10-31 18:04:25 hwiechers

お役立ち情報フレームワークのバージョン4で確認します。 –

これは奇妙に見えます。残念ながら、Code ContractsのVS2010のProバージョンを使用していますので、cccheck自分自身を再生することはできません。

foreachループを使用するのではなく、インデックスが必要なのは間違いありませんか？

これまでの単純化した例でも同じエラーが発生していますか？単純化によって問題が取り除かれていないことを確認する価値は常にあります:)例えば、stuffに契約書チェッカーがstuff.Countについての保証を無効にするために使用する可能性のあるものは何ですか？

出典

2009-08-04 21:59:37

はい、私は、この単純化されたバージョンがまさにそのことを確認しました。これは静的チェッカーのバグです。この場合、私は列挙型を使うことができますが、私には "正しい方法"はインデックスでアクセスするように思われます（私は順番にそれにアクセスしています）。 –

'foreach'はアクセス時に順序付けられます（リストのような）自然順序付けされたコレクション。あなたは、セットのようなものでは失敗することを心配する必要があります。しかし、それはポイントの横にある。コメント行のコメントを外すとどうなりますか？ –

どちらも効果がありません。それはまさに私がバグかもしれないと思った理由です。 –

この契約を証明するには何が必要ですか？必要ですか？

答えて

関連する問題