Code Contracts静态检查器似乎没有意识到ReadOnlyCollection <T>构造函数的Contract.Ensures

Question

我最近安装了代码合同工具(.NET代码合同)和代码合同编辑器扩展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构造对象的属性确保等于参数的Count属性list:

也就是说,静态检查器应该能够判断returnValue.Count == 4(即确保Foo)是否成立.如果我取消注释第二个假设,警告确实会消失,但假设我的方法的确保非常正确,则会违背静态检查器的目的.

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

我试图修改项目范围的额外合同库路径设置无济于事,我认为这不是解决问题的正确方法.

我是否正确地说我的理由是静态检查器没有与合同参考组件正确配置或者我错过了其他的东西？如果我是对的,我将如何修复配置？

我正在使用

• 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>构造函数的确保.它可能是静态分析仪中的错误吗？

Answer 1

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

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