确保IEnumerable不为空的合同

Question

给定的代码

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

发出以下警告:

warning : CodeContracts: requires unproven: Any(source)

如果我删除.Select()它,它就会消失.

但目前还不清楚我究竟是什么,我需要.Ensure这样的cccheck很满意.

Answer 1

你能用这段代码避免警告吗？

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