Contract that ensures the IEnumerable is not empty

Question

The given code

static public int Q()
{
    return Enumerable.Range(0, 100)
        .Select(i => i)
        .First();
}

emits the following warning:

warning : CodeContracts: requires unproven: Any(source)

If I remove .Select() clause it disappears.

But it's not clear to me what exactly I need to .Ensure so that the cccheck was satisfied.

Answer 1

Can you avoid the warning with this code?

var res = Enumerable.Range(0, 100).Select(i => i).Take(1); //execute one query with TOP1 and store in memory
Contract.Assume(res.Any()); //or res.Count() > 0 //query already in memory
return res.First(); //query already in memory