.NET代碼合同：它能比這個更基礎嗎？

Question

我只是瞎搞在這裏對堆棧溢出回答別人的問題，當我注意到一個靜態驗證警告從我的Visual Studio（2008年）內：

string[] source = { "1", "A", "B" }; 
var sourceObjects = Array.ConvertAll(source, c => new Source(c)).ToArray(); 

我得到的消息需要未經證實的來源！ = null。對我來說這似乎很明顯，情況並非如此。這僅僅是一個例子。另一方面，一些非常漂亮的東西似乎工作得很好。

我使用1.2.20518.12版本（5月18日）。我發現代碼合同非常有趣，但是其他人有過這種情況嗎？您是否認爲當前的實施可以在實踐中使用，或者您現在認爲它們純屬學術嗎？

我做了這個社會的維基，但我想聽到一些意見:)

Answer 1

它更有意義，如果你分裂兩個電話了：

string[] source = { "1", "A", "B" }; 
var tmp = Array.ConvertAll(source, c => new Source(c)); 
var sourceObjects = tmp.ToArray(); 

現在它指向以最後一行爲問題。換句話說，對Array.ConvertAll的調用知道源不爲空，但對ToArray()的調用不知道tmp不會爲空。

（由於在源代碼中使用了source這個名稱，您的示例也會有些混淆 - 即使您將變量調用完全不同的東西，錯誤仍會使用source，因爲它指的是第一個參數Enumerable.ToArray。）

基本上我相信這將在Array.ConvertAll獲得適當的非無效後置條件時起作用。在此之前，這將這樣的伎倆：

string[] source = { "1", "A", "B" }; 
var tmp = Array.ConvertAll(source, c => new Source(c)); 
Contract.Assume(tmp != null); 
var sourceObjects = tmp.ToArray(); 

我同意這種東西很討厭，但我敢肯定，這將迅速提高爲MS增加了越來越多的合同到BCL。重要的是要注意，它是而不是靜態檢查器本身的一個問題。

（事實上，Array.ConvertAll沒有任何先決條件 - 如果你設置了source變量在第二代碼片段爲null以上，它仍然不會抱怨。）已通過書面合同章