代碼合同：IEnumerable.Min上的靜態檢查失敗

我在包含代碼合同的以下代碼中收到一些警告。代碼合同：IEnumerable.Min上的靜態檢查失敗

public static int Min(IEnumerable<int> set) 
{ 
    Contract.Requires(set != null); 
    Contract.Requires(set.Any()); 

    Contract.Ensures(Contract.ForAll(set, x => x >= Contract.Result<int>())); 

    int min = set.Min(); 

    return min; 
} 

static void Main(string[] args) 
{ 
    Console.WriteLine(Min(new int[] {3,4,5})); 
    Console.WriteLine(Min(new int[] {})); // should fail 
}

我得到以下警告：

Requires unproven: set.Any() on Min(new int[] {3,4,5}) 

Ensures unproven: Contract.ForAll(set, x => x > Contract.Result<int>())

兩個問題：

我的後置狀態x> = Contract.Result（），但「保證未經證實的」警告狀態x> Contract.Result（）。（更偉大或平等與更好）這是怎麼發生的？
爲什麼不能在上面的語句中證明set.Any（）？

在此先感謝您。

來源

2012-12-12 mbue

'new int [] {3,4,5}'語句在運行時執行。在編譯時，合同檢查器無法知道* set *的內容，所以它無法驗證該集合是否包含任何數據，更不用說Min（）可以返回有意義的結果 –

謝謝。我添加了Contract.Assume（arr！= null && arr.Any（））;在將數組傳遞給Min（）之前。但我仍然不知道爲什麼確保失敗，爲什麼警告聲明（x> Contract.Result（））而不是（x> = Contract.Result（））如代碼中所述。 – mbue

如果您將IEnumerable設置更改爲int []，則檢查程序成功... –

Ensures子句不適用於所有IEnumerable的開頭。您可以編寫一個IEnumerable，它在第一次枚舉時返回一個序列（例如1, 2, 3），第二次返回另一個列表（例如0）。它是一個具有任意實現的接口。

IEnumerable通常有一個很多（可能產生）的東西在封面上。我不認爲CC可以看透這一點，即使具體運行時類型已知。

CC是否能啓發式推理IEnumerable？這對我來說是新的。如果枚舉多次（在數據庫查詢的情況下，這是很平常的），它將不得不假定一個序列不會改變。

讓我指出一個主觀方面的說明，我發現CC檢查器太有限，無法使用。它會導致瘋狂的麻煩來證明有趣的屬性。它不能很好地處理抽象。

來源

2012-12-12 12:22:29 usr

非常感謝你的這個聲明，你最後一句話幾乎反映了我目前的想法......說實話，靜態檢查器是我看到的有關代碼合同的唯一真正價值。在Contract.Requires/Contract.Ensures上進行運行時檢查，看起來像是替代「if（foo）throw Exception」語句的合成糖。所以我的問題是：如果您沒有看到靜態檢查器的真實價值，Code Contracts提供了什麼真正的好處？ – mbue

@mbue我調查了他們的冷靜因素，因爲我相信基於合同的發展。不幸的是，CC是生產力的淨損失。如果我需要它，我有R＃爲我生成參數無效檢查，並且我在它們有意義的地方撒了些聲明。您可能想要查看微軟Pex，它是* awesome *來調試代碼。它只適用於被測代碼與外部依賴關係（IO）隔離的情況。但在這種情況下，它有很好的機會找到*所有*錯誤（定義爲失敗的測試）。它沒有誤報。 – usr

STATIC代碼檢查器無法確定該集合是否包含任何數據。如果你仔細想想，檢查器不知道各種方法和屬性的作用，除非在方法本身內部定義了一些契約。

在你的情況下，檢查器不知道擴展方法Any（）或Min（）的結果可能是什麼，所以它不能驗證任何需求和確保。

通過更改參數的類型可以減少警告，但最終代碼檢查程序仍然無法確保您的代碼能夠滿足Min（...）的要求。

如果將類型更改爲int []或List，則某些警告可能會消失。下面的代碼返回任何警告：

public static int Min(List<int> set) 
    { 
     Contract.Requires(set != null); 
     Contract.Requires(set.Count>0); 


     Contract.Ensures(Contract.ForAll(set, x => x >= Contract.Result<int>())); 

     int min = set.Min(); 

     return min; 
    } 

    static void Main(string[] args) 
    { 

     Console.WriteLine(Min(new List<int> { })); // should fail 
     Console.WriteLine(Min(new List<int> { 3, 4, 5 })); 
     Console.ReadKey(); 
    }

當然，如果你運行該代碼將失敗並拋出異常，所以也許碼檢驗是足夠聰明來檢測這一點。

如果保持原來的順序，你仍然可以得到一個警告：

 Console.WriteLine(Min(new List<int> { 3, 4, 5 })); 
     Console.WriteLine(Min(new List<int> { })); // should fail

在這兩種情況下，你還可以得到一些瘋狂的建議，比如增加在主Contract.Ensures（假）（）。

來源

2012-12-12 12:47:47

代碼合同：IEnumerable.Min上的靜態檢查失敗

回答

相關問題