不可變方法[ContractInvariantMethod]可以在接口契約內工作嗎？

Question

我正在創建如第號中所述的接口合同2.8接口合同的Feb 4, 2011 Code Contracts User Manual (PDF)。這不是問題。

此外，我想混合一個對象不變（見第4.2 ContractInvariantMethod）到相同的接口合同。這是個問題。我無法找到Interface Interface上使用的Object Invariants的例子。

我試着在以下部分代碼片段中看到的接口契約中添加一個對象不變量。它編譯。在運行時，它不會引發任何錯誤，但它似乎沒有做任何正面的事情（即被調用）。

/* Note: The intention of this snippet is to cause the data implementation 
* to fail if it is not initalized before its public data access methods are called. 
*/ 
[ContractClassFor(typeof(IDataProxy))] 
abstract class IDataProxyContract : IDataProxy 
{ 
    [ContractInvariantMethod] 
    private void ObjectInvariant() 
    { 
     Contract.Invariant(IsInited == true, "Instance not initialized."); 
    } 

我無法找到專門解決這種情況或駁斥它的文檔。

在這一點上，我不確定是否遺漏了一個步驟來使其工作，或者代碼合同技術完全忽略了此對象中的對象不變量。我想使它工作。有人知道答案嗎？

Answer 1

顯然答案是曼努埃爾Fahndrich，微軟（MSFT）回答了DevLabs論壇：

不變對象上不支持目前的接口。我可以 看到他們爲什麼可能會很方便。

Full context and code sample here...

Answer 2

他們是默認關閉的。

我的猜測是契約不是由編譯器選項啓用的，所以它們不會被編入代碼。

的解決方案是從devlabs

• http://msdn.microsoft.com/en-us/devlabs/dd491992

你安裝它後，到項目屬性下載這個包，你會看到另一個標籤。

然後，您可以啓用一個選項：「執行運行時檢查合同：完整的」

Answer 3

不變提供用於約束對象的內部狀態的機制。

他們被視爲實現細節，這就是爲什麼他們在一個私人方法內實施。界面顯然沒有狀態的概念（甚至屬性只是方法的語法糖），因此不能有不變量。在最原始的用途中，不變量用於字段。但是，自動屬性的概念已經明顯模糊了這一線，導致了這種情況下的混亂。

我同意應該有一個更簡潔的承包屬性的方式，只是因爲你的事前和事後條件總是相同。