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

Viewed 782

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?

2 Answers
Related