为什么CodeContracts警告我"需要未经证实:索引<@ this.Count"即使我已经检查了计数？

Question

我的代码看起来像这样:

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'
    }
}

不应该Any为索引0 的支票帐户？我做错了什么,或者CodeContracts是不是认不出这种情况？

Answer 1

LINQ .Any和项目访问器[0]是不相关的,没有使代码契约认为它们是相同的东西.因为this.bar无论如何都会使用默认值进行初始化,所以最好这样做:

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

这不仅可以解决AakashM指出的线程安全的可能性,而且还可以提高性能.既然你知道this是一个集合(因此有一个.Count),另一种选择是:

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

Answer 2

LINQ方法都没有使用ContractsAPI 进行注释.因此,当验证程序在此方法上运行时,它不会获取有关该值的新数据Count.这就是你看警告的原因.

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

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