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