代碼合同和規範之間的差異＃

Question

我想在C＃中實現DBC。我面對它的規範和代碼合同。
Spec＃和Code Contract之間的區別是什麼？

Answer 1

這是從Code Contracts FAQs at Microsoft Research：

待辦事項代碼契約有什麼用規格＃？

代碼合同是來自Spec＃項目的衍生產品。 Spec＃的研究重點是在 繼承，回調，別名和多線程的存在下理解對象不變量的含義。 Spec＃是C＃2.0版的 超集，並使用源級重寫器將 合約編織到代碼中。它使用驗證條件生成和 定理證明器來進行Spec＃代碼的靜態驗證。但是 與維護對象 不變的所有複雜問題妥善處理不變價格：驗證變得不平凡。這就是爲什麼 規範＃還需要一個所有權規定，以知道哪些對象可能是別名或不能相互混淆的。

代碼合同是從規範＃學習的結果，什麼工作和 什麼沒有。與規範＃不同，代碼契約是語言不可知的，因此可以跨所有.NET語言工作，從VB到C＃到F＃。重寫器 適用於MSIL，因此不依賴於特定的編譯器。它的 靜態分析引擎使用抽象解釋，這比驗證更快，更可預測;此外，抽象 的解釋推斷環路不變量和方法合同，其中 有助於代碼合同的採用和易用性。

因此，Code Contracts似乎是未來更受「支持」的工具。