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

Answer 2

Since this solves the problem and is still not that ugly as one might have thought initially, I'm posting it as an answer (if one has better ideas I'm open for your suggestions though):

static public int Q()
{
    var e = Enumerable.Range(0, 100)
        .Select(i => i);

    Contract.Assume(e.Any());
    return e.First();
}

So I should not have to split the whole expression, but the part that the static analyzer was afraid of, and for that part I could assure it that it's "all fine, trust me, I know what I'm doing".

A note:

for some reason neither

Contract.Assert(e.Count() > 0);

or

Contract.Assert(e.Any());

work.

Important: as other people mention, this might be not suitable for all cases, since the additional e.Any() call would materialize the collection, which may be undesirable in some cases (eg: when it's a LINQ from a 3rd party source).