c# - 确保 IEnumerable 不为空的契约(Contract)

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