contratto che assicura l'IEnumerable non è vuota

Question

Il dato codice

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

emette il seguente avviso:

warning : CodeContracts: requires unproven: Any(source) 

Se rimuovo .Select() clausola scompare.

Ma non è chiaro per me esattamente ciò che è necessario per .Ensure in modo che il cccheck è stato soddisfatto.

Answer 1

si può evitare l'avvertimento con questo codice?

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

Dal momento che questo risolve il problema e non è ancora quel brutto come si sarebbe potuto pensare inizialmente, sto postando come una risposta (se uno ha idee migliori sono aperto per i suggerimenti però):

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

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

Quindi io non avrei dovuto dividere l'intera espressione, ma la parte che l'analizzatore statica temeva, e per quella parte ho potuto assicurare che che è "tutto bene, fidati di me, so quello che sto facendo" .

Una nota:

per qualche motivo non

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

o

Contract.Assert(e.Any()); 

lavoro.

Importante: come altre persone parlare, questo potrebbe non essere adatto per tutti i casi, dal momento che l'ulteriore e.Any() chiamata sarebbe materializzarsi la raccolta, che può essere indesiderabile in alcuni casi (ad esempio: quando si tratta di un LINQ da un 3rd party fonte).