5

最近コード コントラクト ツール (コード コントラクト for .NET) とコード コントラクト エディター拡張機能 VS2012 をインストールしましたが、静的チェッカーを正しく動作させるのに問題があります。

次のコードで Code Contracts の静的チェッカーを実行すると (2 番目の仮定はコメント化されています)

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

「証明されていないことを保証する」という警告が表示されます。

CodeContracts: 証明されていないことを保証します:Contract.Result<ReadOnlyCollection<byte>>().Count == 4

Fooメソッドの確実性は証明されていないと主張しています。ただし、 のコンストラクターにマウスを合わせるReadOnlyCollection<T>と、構築されたオブジェクトのプロパティがパラメーターのプロパティCountと等しいことが保証されていることがわかります。Countlistコンストラクターのマウスオーバー

つまり、静的チェッカーは、returnValue.Count == 4(つまり の保証Foo) が真であると判断できる必要があります。2 番目の仮定のコメントを外すと、警告は消えますが、メソッドの保証が真であると仮定すると、静的チェッカーの目的が大きく損なわれます。

問題は、エディター拡張機能のみが、コンストラクター (mscorlib.Contracts.dll) の保証を含むコントラクト参照アセンブリを認識しているため、静的チェッカーが認識していないコントラクトをリストすることであると思います。

プロジェクト全体の Extra Contract Library Paths 設定をいじってみましたが、うまくいきませんでした。それが問題を解決する正しい方法だとは思いません。

静的チェッカーがコントラクト参照アセンブリで適切に構成されていないという私の推論は正しいですか、それとも他に何か不足していますか? 私が正しければ、どのように構成を修正しますか?

私は使用しています

  • Visual Studio Ultimate 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>今私が疑問に思っているのは、なぜ静的チェッカーがコンストラクターの保証を認識しないのかということです。静的アナライザーのバグでしょうか?

4

1 に答える 1

0

ReadOnlyCollectionクラスの Count プロパティが定数ではないため、Code Contracts がこの警告を発している可能性があります。

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

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();
于 2016-03-01T23:11:37.213 に答える