靜態檢查契約式設計

Question

最近我被這個想法激動的在.NET 4.0/Visual Studio 2010中

不過我傷心地發現，它只會在Visual Studio中提供的合同靜態檢查設計團隊系統。 http://msdn.microsoft.com/en-us/devlabs/dd491992.aspx

是否有任何替代方案通過合同爲c＃提供靜態檢查設計？

單聲道項目是否將這種功能添加到那裏編譯器？

Answer 1

他指的是定理證明。

沒有什麼能夠阻止開放源代碼或商業社區實施他們自己的。合同類是BCL的一部分，並且非常容易添加到Mono中。如果我們想靜態檢查一些事情，「我們將」需要制定一個定理證明。

證明者不是編譯器的一部分。它基本上運行如下：

• 編譯與CONTRACTS_FULL定義的二進制版本。這會發出所有合約屬性並調用Contract類靜態方法。
• 加載程序集「僅用於反射」，並解析所有方法的字節碼。具有狀態信息的詳細流程分析將允許某些合同被顯示爲「始終正確」。有些人會「在某些時候被認爲是虛假的」。其他人將「無法靜態證明合同」。

隨着工具變得越來越好，它將從對每個合同發出警告，最終向Microsoft版本提供類似的證明結果。

編輯：男人，如果反射器是開源的，這將是偉大的。第一遍實現當然可以作爲插件運行。這樣，可以設計證明者邏輯而不用擔心二進制文件如何加載。一旦它證明有功能（得到它），就可以提取和構建邏輯，以便對另一個組裝加載器（開源的）生成的語法樹進行操作。這裏重要的/新穎的東西是證明邏輯 - 裝配加載器已經完成了多次，並沒有什麼變化壯觀的用途。

Answer 2

代碼契約不需要C＃編譯器，因爲它們是作爲.NET Framework 4.0中的類實現的。任何可以發出託管程序集的.NET編譯器都是可用的，儘管在混合託管代碼和本地代碼時C++/CLI可能會發出不兼容的程序集。

IDE還執行了其他工具來重寫生成的IL，以便合同出現在正確的位置，因此Mono項目作者需要編寫類似的工具，以便合同在Mono平臺上工作。

有關更多信息，請參閱this post。