この契約アサーションを証明できないのはなぜですか？

Question

私はこのようになりますクラスを持っている：

class Foo 
{ 
    private IEnumerable<Bar> bars; 

    ... 

    private void DoSomething() 
    { 
     Contract.Requires(bars != null); 
     Contract.Requires(bars.Any()); 

     Bar result = bars.FirstOrDefault(b => SomePredicate) ?? bars.First(); 
     Contract.Assert(result != null); // This asserts fails the static checker as "cannot be proven" 
    } 
} 

私の知る限り、契約それはresultがnullでないことを知るために必要なすべての情報を持っています。 barsには少なくとも1つの要素があります。これらの要素のいずれかがSomePredicateに一致する場合は、resultが最初の要素になります。そうでない場合、resultはbarsの最初の要素になります。

なぜアサーションが失敗するのですか？

Answer 1

barsの要素がnullでないことを保証または仮定していません。試してみてください：

Contract.ForAll(bars, x => x != null); 

か（実際不変）：

Contract.Requires(bars.FirstOrDefault(x => SomePredicate(x)) != null 
       || bars.First() != null); 

Answer 2

barsには、まだnullという項目が含まれている可能性があります。その項目が最初の項目である場合、resultはまだnullになります。

Answer 3

barsの最初の要素がnullの場合はどうなりますか？ （A：アサーションが失敗します。）