c# - 代码契约(Contract)静态检查器似乎没有意识到 ReadOnlyCollection 构造函数的 Contract.Ensures

Question

我最近安装了 Code Contracts Tools(.NET 代码契约(Contract))和 Code Contracts Editor Extensions VS2012，但我在让静态检查器正常工作时遇到了一些问题。

当我对以下代码运行 Code Contracts 的静态检查器时(第二个假设已被注释掉)

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: ensures unproven: Contract.Result<ReadOnlyCollection<byte>>().Count == 4

它声称 Foo 的保证方法未经证实。但是，当我将鼠标悬停在 constructor 上时的 ReadOnlyCollection<T> ，我可以说 Count确保构造对象的属性等于 Count list 的属性(property)参数:

也就是说，静态检查器应该能够分辨出 returnValue.Count == 4 (即 Foo 的保证)成立。如果我取消对第二个假设的注释，警告会消失，但假设我的方法的确保成立非常违背静态检查器的目的。

我认为问题可能是只有编辑器扩展知道包含构造函数 (mscorlib.Contracts.dll) 确保的契约(Contract)引用程序集，因此它列出了静态检查器不知道的契约(Contract).

我已经尝试修改项目范围的额外契约(Contract)库路径设置但无济于事，我认为这不是解决问题的正确方法。

我的推理是否正确，即静态检查器未正确配置契约(Contract)引用程序集，还是我遗漏了其他内容？如果我是对的，我将如何修复配置？

我正在使用

• Visual Studio Ultimate 2012 更新 3
• 代码契约(Contract)工具版本 1.5.60502.11
• Code Contracts Editor Extensions VS2012 版本 1.5.64024.12

编辑: 静态检查器似乎确实找到了契约(Contract)引用程序集，并且它的工作方式与我最初预期的一样，它可以与其他类甚至 ReadOnlyCollection<T> 的方法一起工作。类(class)。例如，以下方法的静态分析就可以正常工作。

    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> 的确保构造函数。会不会是静态分析器的bug？

Answer 1

Code Contracts 可能会引发此警告，因为 ReadOnlyCollection 类的 Count 属性不是常量。

在下面的示例中，我创建了一个 ReadOnlyCollection 类的实例，并传递了一个包含 4 个整数的列表。 Count 属性返回值 4。我随后通过清除 ReadOnlyCollection 并添加 3 个整数来修改 wrapped 列表。 ReadOnlyCollection 的 Count 属性现在返回值 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();