为什么 CodeContracts 警告我“需要未经验证:索引 <” @this.Count”即使我已经检查过计数?

发布于 2024-11-26 15:06:39 字数 467 浏览 1 评论 0 原文

我的代码看起来像这样:

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 只是不识别这种情况?

I have code that looks something like this:

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? Am I doing something wrong, or does CodeContracts just not recognize this case?

如果你对这篇内容有疑问,欢迎到本站社区发帖提问 参与讨论,获取更多帮助,或者扫码二维码加入 Web 技术交流群。

扫码二维码加入Web技术交流群

发布评论

需要 登录 才能够评论, 你可以免费 注册 一个本站的账号。

评论(2

ˇ宁静的妩媚 2024-12-03 15:06:39

LINQ 的 .Any 和项目访问器 [0] 没有足够的相关性,以至于代码契约尚未将它们视为同一事物。由于 this.bar 无论如何都会使用默认值进行初始化,因此最好这样做:

Contract.Requires(items != null);
this.bar = items.FirstOrDefault();

这不仅可以解决 AakashM 指出的线程安全的可能性,而且还稍微多了一点表现出色。由于您知道 this 是一个集合(因此有一个 .Count),另一个选项是:

if(this.Count > 0)
    this.bar = this[0]; 

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. Since this.bar would be initialized using a default value anyway, it's probably best to just do this:

Contract.Requires(items != null);
this.bar = items.FirstOrDefault();

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:

if(this.Count > 0)
    this.bar = this[0]; 
乙白 2024-12-03 15:06:39

所有 LINQ 方法均未使用 Contracts API 进行注释。因此,当验证程序在此方法上运行时,它不会获取有关 Count 值的新数据。这就是您看到警告的原因。

解决此问题的一种方法是使用 Assume 告诉验证者此时计数是有效的。

if (this.Any()) {
  Contract.Assume(this.Count > 0);
  this.bar = this[0];
}

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 of Count. 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.

if (this.Any()) {
  Contract.Assume(this.Count > 0);
  this.bar = this[0];
}
~没有更多了~
我们使用 Cookies 和其他技术来定制您的体验包括您的登录状态等。通过阅读我们的 隐私政策 了解更多相关信息。 单击 接受 或继续使用网站,即表示您同意使用 Cookies 和您的相关数据。
原文