如何確保迭代器方法不會產生任何空項目？

我想知道是否有可能確保（使用code-contracts）迭代器方法永遠不會產生空項目。如何確保迭代器方法不會產生任何空項目？

這種簡化的方法：

public static IEnumerable<object> CreateSomeObjects() 
{ 
    Contract.Ensures(Contract.Result<IEnumerable<object>>() != null); 
    Contract.Ensures(Contract.ForAll(Contract.Result<IEnumerable<object>>(), _ => _ != null)); 

    for (int i = 0; i < 10; ++i) 
    { 
     yield return new object(); 
    } 
}

產生編譯時間警告類似：

CodeContracts：MyClass.CreateSomeObjects（）[0x9]：確保未經證實：Contract.ForAll（合同.Result>（），_ => _！= null）

我該怎麼做才能向靜態檢查器證明它？

來源

2015-11-07 Mårten Wikström

我試圖讓這個相同的東西工作，但對我來說它甚至沒有給出任何編譯時間的警告。經過大量搜索後，我最終使用了不帶代碼合同的不同解決方案，因爲我根本無法找到解決方案。我會嘗試使用遺留代碼來檢查代碼合同塊內是否不爲null，並用'Contract.EndContractBlock（）'關閉它。 https://msdn.microsoft.com/en-us/library/system.diagnostics.contracts.contract.endcontractblock(v=vs.110).aspx。讓我知道這個是否奏效！ – anthonytimmers

只有這樣，你可以把迭代器合同是：上述

public class Graph 
{ 
    public IEnumerable<Node> Nodes(Graph g) 
    { 
     Contract.Requires(g != null); 
     Contract.Ensures(Contract.ForAll(Contract.Result<IEnumerable<Nodei>>, node => node != null)); 
     foreach (var x in g.MethodForGettingNodes()) 
     yield return x; 
    } 
}

的合同確保呼叫者不空參數傳遞和方法本身保證所產生的集合中的所有元素非空。

目前，靜態檢查器沒有對收集進行推理，因此將無法證明上述後置條件。

根據文檔，他們仍然沒有解決它自2009年以來，我有問題與cc 2年前，他們仍然沒有解決它，我認爲他們不會。

來源

2015-11-08 01:44:40

謝謝。爲了清楚起見，文檔（http://download.microsoft.com/download/C/2/7/C2715F76-F56C-4D37-9231-EF8076B7EC13/userdoc.pdf）在第6.6.1節中說：當使用C＃編寫迭代器時，產出支持靜態合約檢查器不會能夠證明後置條件。 –

我想知道，如果你在'foreach'循環內部'Contract.Assert（x！= null）'，在'yield return x'之前會發生什麼？ – fourpastmidnight

如何確保迭代器方法不會產生任何空項目？

回答

相關問題