为什么 CodeContracts 警告我“需要未经验证:索引 <” @this.Count”即使我已经检查过计数?
我的代码看起来像这样:
public class Foo<T> : ObservableCollection<T>
{
private T bar;
public Foo(IEnumerable<T> items)
: base(items.ToList())
{
Contract.Requires(items != null);
if (this.Any())
this.bar = this[0]; // gives 'requires unproven: index < @this.Count'
}
}
Shouldn't the Any
check account for index 0?我是否做错了什么,或者 CodeContracts 只是不识别这种情况?
如果你对这篇内容有疑问,欢迎到本站社区发帖提问 参与讨论,获取更多帮助,或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱,如果其他用户或者作者回复了您的评论,将不能在第一时间通知您!
发布评论
评论(2)
LINQ 的
.Any
和项目访问器[0]
没有足够的相关性,以至于代码契约尚未将它们视为同一事物。由于this.bar
无论如何都会使用默认值进行初始化,因此最好这样做:这不仅可以解决 AakashM 指出的线程安全的可能性,而且还稍微多了一点表现出色。由于您知道
this
是一个集合(因此有一个.Count
),另一个选项是:LINQ's
.Any
and the item accessor[0]
are unrelated enough that Code Contracts hasn't been made to consider them to be the same thing. Sincethis.bar
would be initialized using a default value anyway, it's probably best to just do this:This would not only resolve the possibility of thread-safety which AakashM points out, but it is also slightly more performant. Since you know
this
is a collection (and therefore has a.Count
), another option would be:所有 LINQ 方法均未使用
Contracts
API 进行注释。因此,当验证程序在此方法上运行时,它不会获取有关Count
值的新数据。这就是您看到警告的原因。解决此问题的一种方法是使用
Assume
告诉验证者此时计数是有效的。None of the LINQ methods are annotated with the
Contracts
API. Hence when the verifier runs on this method it acquires no new data about the value ofCount
. This is why you see the warning.One way to work around this is to use
Assume
to tell the verifier the count is valid at this point.