需要什么来证明本合同的要求？
我有一个在锦标赛中运行的应用程序，并且我收到了有关此简化代码结构的合同警告：
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 上证明这一点？ 这是静态分析器中的错误吗？ 我如何向 Microsoft 提交错误报告？
I have an application that runs through the rounds in a tournament, and I am getting a contract warning on this simplified code structure:
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());
}
}
The warning is:
contracts: requires unproven: index < @this.Count
What am I doing wrong? How can I prove this on an IList<T>? Is this a bug in the static analyzer? How would I submit a bug report to Microsoft?
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（2）
这看起来确实很奇怪。 不幸的是，我使用的是带有代码契约的 VS2010 专业版，所以我无法自己运行 cccheck 来玩。
您确实需要索引而不仅仅是使用
foreach循环吗？只是为了确定 - 上面的简化示例是否会产生相同的错误？ 总是值得检查一下简化是否没有消除问题:) 例如，您是否对
stuff做了任何其他事情，合同检查器可能会使用这些来使有关stuff.Count< 的保证无效/代码>?That does look odd. Unfortunately I'm using the Pro version of VS2010 with Code Contracts, so I can't run
cccheckmyself to play around.Do you definitely need the index rather than just using a
foreachloop?Just to be sure - does your simplified example above produce the same error? It's always worth checking that the simplification hasn't removed the problem :) For instance, do you do anything else to
stuffwhich the contract checker might use to invalidate the guarantee aboutstuff.Count?我用代码合约版本 1.2.21023.14 检查了这一点，没有收到警告。 我的猜测是这是一个错误，现已修复。
I checked this with version 1.2.21023.14 of code contracts and didn't get warnings. My guess is that it is a bug that has since been fixed.