Contract.Ensures如何工作？

我開始使用代碼合同，雖然Contract.Requires非常簡單，但我很難看到確保實際執行的操作。Contract.Ensures如何工作？

我試圖創建這樣一個簡單的方法：

static void Main() 
{ 
    DoSomething(); 
} 

private static void DoSomething() 
{ 
    Contract.Ensures(false, "wrong"); 
    Console.WriteLine("Something"); 
}

我從來沒有看到消息「錯誤的」，雖然，也不拋出異常或其他任何東西。

那它究竟做了什麼？

來源

2011-08-13 Steffen

我開始你的例子，並得到一個未處理的異常'ContractException'「後置失敗：錯誤的」寫入控制檯後的東西。所以看起來很好。 –

靜態證明器是代碼合約背後的真正價值，雖然這種特殊的確保條件很奇怪，從分析的角度來看。這大致相當於要求一個人證明「這個陳述是錯誤的」的真相。 –

錯誤的部分只是爲了確保它被觸發:-) – Steffen

奇怪的是它不會拋出任何東西 - 如果您正在運行重寫器工具並進行適當的設置。我的猜測是，你運行的模式不檢查後置條件。

的令人困惑的事情有關Contract.Ensures是你寫它在方法的開端，但它在方法結束執行。重寫器會執行所有的魔術來確保它正確執行，並在必要時給出返回值。

與代碼合同的許多事情一樣，我認爲最好在重寫器工具的結果上運行Reflector。確保你的設置正確，然後確定重寫器做了什麼。

編輯：我意識到我沒有表達點Contact.Ensures呢。簡而言之，就是確保你的方法最終完成了某些事情 - 例如，它可以確保它向列表中添加了某些內容，或者（更可能）確保返回值非空，或者是正值或其他值。例如，你可能有：

public int IncrementByRandomAmount(int input) 
{ 
    // We can't do anything if we're given int.MaxValue 
    Contract.Requires(input < int.MaxValue); 
    Contract.Ensures(Contract.Result<int>() > input); 

    // Do stuff here to compute output 
    return output; 
}

在重寫代碼，就會有回報時的點檢查以確保返回的值確實是大於輸入。

來源

2011-08-13 19:05:32

你是對的 - 模式在項目設置中設置錯誤。愚蠢的錯誤在我身上:-) – Steffen

@Steffen：我增加了一些，使其更清楚它的意義。我不知道你是否需要這樣做，但可能未來的讀者可能會覺得它有用:) –

好的闡述 - 這是我期望它做的非常多，但它總是寫得很好:-) – Steffen

Contract.Ensures如何工作？

回答

相關問題