5

我最近安装了代码合同工具（.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）的确保的合同引用程序集，所以它列出了静态检查器不知道的合同。

我尝试修改项目范围的 Extra Contract Library Paths 设置无济于事，我认为这不是解决问题的正确方法。

我的推理是正确的，即静态检查器没有使用合同参考程序集正确配置，还是我遗漏了其他东西？如果我是对的，我将如何修复配置？

我在用着

  • Visual Studio 终极版 2012 更新 3
  • 代码合同工具版本 1.5.60502.11
  • Code Contracts Editor Extensions 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 属性不是常量。

在下面的示例中，我创建了一个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();
于 2016-03-01T23:11:37.213 回答