代码合同静态检查器似乎不知道ReadOnlyCollection<T>构造函数中的Contract.Ensures。

Question

我最近安装了Code Contracts工具（.NET的代码合同）和Code Contracts编辑器扩展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: 确保未经证明：Contract.Result<ReadOnlyCollection<byte>>().Count == 4

它声称 Foo 方法的确保未经证明。然而，当我将鼠标悬停在 ReadOnlyCollection<T> 的 构造函数 上时，我可以知道所构造对象的 Count 属性被确保等于 list 参数的 Count 属性：

也就是说，静态检查器应该能够判断 returnValue.Count == 4（即 Foo 的确保）为真。如果我取消第二个假设，则警告会消失，但假设我的方法的确保为真非常有违静态检查器的初衷。

我认为问题可能在于只有编辑器扩展程序知道包含构造函数保证的合同引用程序集（mscorlib.Contracts.dll），因此它列出了静态检查器不知道的合同。我尝试过调整项目范围内的额外合同库路径设置，但没有任何效果，我认为那不是解决问题的正确方法。我的推理是否正确，静态检查器没有正确配置合同引用程序集，还是我漏掉了其他东西？如果我是正确的，我该如何修复配置？我正在使用Visual Studio Ultimate 2012 Update 3、Code Contracts Tools版本1.5.60502.11和Code Contracts Editor Extensions VS2012版本1.5.64024.12。编辑：静态检查器似乎可以找到合同引用程序集，并且它与ReadOnlyCollection 类的其他类甚至方法一样正常工作。例如，以下方法的静态分析完全正常。

    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 构造函数的确保。这可能是静态分析器中的错误吗？

- Sam

Answer 1

代码合同可能会引发此警告，因为ReadOnlyCollection类的Count属性不是常量。

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

- Ɖiamond ǤeezeƦ