c# - 证明这个 Contract.Requires 需要什么？

Question

我有一个在锦标赛中运行的应用程序，我收到了关于这个简化代码结构的合同警告：

    public static void LoadState(IList<Object> stuff)
    {
        for(int i = 0; i < stuff.Count; i++)
        {
            // Contract.Assert(i < stuff.Count);
            // Contract.Assume(i < stuff.Count);

            Object thing = stuff[i];

            Console.WriteLine(thing.ToString());
        }
    }

警告是：

contracts: requires unproven: index < @this.Count

我究竟做错了什么？我怎样才能证明这一点IList<T>？这是静态分析器中的错误吗？如何向 Microsoft 提交错误报告？

Answer 1

这看起来确实很奇怪。不幸的是，我正在使用带有代码合同的专业版 VS2010，所以我不能自己cccheck玩。

您是否确实需要索引而不仅仅是使用foreach循环？

只是为了确定-您上面的简化示例是否会产生相同的错误？检查简化并没有消除问题总是值得的 :) 例如，您是否做了任何其他stuff合同检查员可能用来使担保无效的事情stuff.Count？

Answer 2

我使用 1.2.21023.14 版本的代码合同对此进行了检查，但没有收到警告。我的猜测是这是一个已经修复的错误。