如何向CodeContracts證明IEnumerable <T>.Single（）永不返回空？

我有下面的代碼片段：如何向CodeContracts證明IEnumerable <T>.Single（）永不返回空？

public static string returnString() 
    { 
     string[] stringList = { "a" }; 

     if (stringList.Count() != 1) 
     { 
      throw new Exception("Multiple values in list"); 
     } 

     var returnValue = stringList.Single(); 

     Contract.Assert(returnValue != null, "returnValue is null"); 

     return returnValue; 
    }

CodeContract說：

CodeContracts：斷言證實。你是否在Single上假設靜態檢查器不知道？

在我的理解中，Single()永遠不會返回null - 它返回IEnumerable的唯一值，或者它會拋出異常。我如何向代碼分析器證明這一點？

來源

2015-05-18 Rufus Buschart

'Single' _can_如果集合僅包含空值，則返回null。 –

看起來像靜態分析器不足以知道'stringList'被硬編碼爲只包含''a「'。可以說是代碼合同中的一個錯誤。 –

也可以爭辯說，在考慮上面的邊界情況時，兩種驗證都可以合併爲SingleOrDefault（）的單個調用和null上的斷言。 – moarboilerplate

在我的理解，Single()從不返回null

事實並非如此 -

string[] a = new string[] {null}; 

bool check = (a.Single() == null); // true

它返回要麼恰好只有IEnumerable的值或者拋出一個異常。

這是正確的 - 所以，如果集合只包含一個空值則Single將返回null。

來源

2015-05-18 16:02:52

這真的很聰明！我從來沒有考慮過Single（）的可能結果。 –

我認爲人們認爲所有Linq方法都不會返回null，因爲返回_collection_的方法將返回一個空集合而不是'null'。返回_value_（'First（）'，'Single（）'等）的方法當然可以返回null。 –

如何向CodeContracts證明IEnumerable <T>.Single（）永不返回空？

回答

相關問題