Why does CodeContracts warn me that "requires unproven: index < @this.Count" even though I have already checked the count?

Question

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?

Answer 1

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]; 

Answer 2

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];
}