爲什麼不能證明這個合同聲明？

我有一個類，它看起來是這樣的：爲什麼不能證明這個合同聲明？

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不會是空的信息。 bars至少有一個元素。如果其中一個元素匹配SomePredicate，result將是第一個這樣的元素。如果不是，result將成爲bars中的第一個元素。

爲什麼斷言失敗？

來源

2011-07-28 Matthew Pirocchi

您尚未確保或假定bars中的元素不爲空。嘗試：

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

或（實際不變）：

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

來源

2011-07-28 14:54:55 user7116

或'Contract.Requires（bars.Any（X => X = NULL）！）' – leppie

@leppie：要麼就是那些表單首選？我在用戶文檔中找到的所有內容是「也可以使用擴展方法'System.Linq.Enumerable.Any'而不是'Contract.Exists'。」 –

@Matthew：如果永遠不可能有空元素，則使用ForAll，否則使用Any。使用'Any'時，你還必須在代碼的後半部分有'First（x => x！= null）'。細微差別。 – leppie

收集bars仍然可能包含一個項目是null。如果該項目是第一項，那麼result仍然可以是null。

來源

2011-07-28 14:54:15 Sven

如果bars的第一個元素是null會怎麼樣？（A：斷言失敗。）

來源

2011-07-28 14:54:31 dlev

爲什麼不能證明這個合同聲明？

回答

相關問題