コード契約静的チェッカーは一見Contract.EnsuresのReadOnlyCollection <T>コンストラクタ

Question

私は最近Code Contracts Tools（.NET用コード契約）とCode Contracts Editor Extensions VS2012をインストールしました。静的チェッカーを動作させるにはいくつかの問題があります正しく。

CodeContracts：：私は

using System.Collections.Generic; 
using System.Collections.ObjectModel; 
using System.Diagnostics.Contracts; 

public class TestClass 
{ 
    public ReadOnlyCollection<byte> Foo() 
    { 
     Contract.Ensures(Contract.Result<ReadOnlyCollection<byte>>().Count == 4); 

     IList<byte> list = new byte[4]; 
     Contract.Assume(list.Count == 4); 
     var returnValue = new ReadOnlyCollection<byte>(list); 
     //Contract.Assume(returnValue.Count == 4); 
     return returnValue; 
    } 
} 

（コメントアウト第2の仮定で）次のコードでコードコントラクト静的チェッカーを実行すると

私は警告読み 『証明されていないが保証さ』を取得性を保証証明されていない：Contract.Result<ReadOnlyCollection<byte>>().Count == 4

Fooメソッドの保証は実証されていないと主張しています。しかし、I ReadOnlyCollection<T>のconstructor上にマウス、Iが構築されたオブジェクトのCountプロパティはlistパラメータのCount性と等しくなるように確保されていることを伝えることができる。

すなわち、静的チェッカがあるべきですreturnValue.Count == 4（すなわち、保証はFoo）が成立していることを伝えることができます。私が第2の仮定のコメントを外すと、警告は消えますが、私の方法の保証が真実であると仮定すると、静的チェッカーの目的をはるかに凌駕します。

エディタ拡張だけがコンストラクタ（mscorlib.Contracts.dll）の保証を含む契約参照アセンブリを認識しているので、静的チェッカーが認識していないコントラクトがリストされている可能性があります。

私は、プロジェクト全体のExtra Contract Library Paths設定を無駄にしようと試みましたが、問題を解決する正しい方法ではないと思います。

静的チェッカーが契約参照アセンブリで正しく構成されていないか、他に何か不足していますか？私が正しいとすれば、設定を修正するにはどうすればいいですか？

私は

• を使用しているVisual Studioの究極の2012 Update 3の
• コードは、ツールのバージョン1.5.60502.11
• コード・エディタの拡張機能VS2012バージョン1.5.64024.12

を契約コントラクト編集：静的チェッカーは、契約参照アセンブリを見つけるように見えます、そして、私が最初に期待したように動作します他のクラス、さらにはReadOnlyCollection<T>クラスのメソッドでも同じです。例えば、以下のメソッドの静的解析はうまく動作します。コンストラクタの性を保証がまだ動作しませんので、

public int Boo() 
    { 
     Contract.Ensures(-1 <= Contract.Result<int>()); 
     Contract.Ensures(Contract.Result<int>() < 4); 

     IList<byte> list = new byte[4]; 
     var collection = new ReadOnlyCollection<byte>(list); 
     Contract.Assume(collection.Count == 4); 
     return collection.IndexOf(0); 
    } 

Countプロパティに関する仮定が必要です。一方、IndexOfメソッドの保証は非常にうまくいきます。

ここで、スタティックチェッカーがReadOnlyCollection<T>コンストラクタの保証を認識しないのはなぜですか？スタティック・アナライザのバグでしょうか？

Answer 1

ReadOnlyCollectionクラスのCountプロパティが定数ではないため、この警告が表示される可能性があります。

以下の例では、ReadOnlyCollectionクラスのインスタンスを作成し、4つの整数を含むリストを渡します。 Countプロパティは値4を返します。その後、リストをに変更してReadOnlyCollectionに変更し、それをクリアして3つの整数を追加します。 ReadOnlyCollectionのCountプロパティは、ReadOnlyCollectionに触れずに3の値を返すようになりました。

IList<byte> list = new List<byte>() { 1, 2, 3, 4 }; 
var collection = new ReadOnlyCollection<byte>(list); 

// Outputs: 1, 2, 3, 4. 
foreach (var item in collection) 
{ 
    Console.WriteLine(item); 
} 

list.Clear(); 
list.Add(5); 
list.Add(6); 
list.Add(7); 

// Outputs: 5, 6, 7 
Console.WriteLine(); 
foreach (var item in collection) 
{ 
    Console.WriteLine(item); 
} 

Console.ReadKey();