c# - 需要什么来证明本契约(Contract)的要求？

Question

我有一个在锦标赛中运行的应用程序，并且我收到了有关此简化代码结构的契约(Contract)警告:

    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 做了任何其他事情，契约(Contract)检查器可能会使用这些来使有关 stuff.Count< 的保证无效？