代碼合同 - 是否應檢查私有方法的前置條件和後置條件？

Question

我正在努力加快代碼合同的速度。我喜歡這個概念，但在實踐中，我看不到在許多私有方法中增加Contract.Requires的價值，其中一些方法只有一兩行。

我可以看到關於公共方法的一點，但在私有類方法上，它似乎是矯枉過正。

Answer 1

你想要的合同適用於私有方法的主要理由是，如果你正在做靜態分析的優勢。您經常會編寫隱含的有關您的私有方法的代碼（例如，此方法永遠不會返回null），並且靜態證明程序會將其指出給您。然後，您可以將假設置於公共方法的正文中，也可以將其作爲合同添加到私有方法中。後者通常比較乾淨，因爲它允許您在多次使用該私有方法的過程中重用合同暗示的假設。

就我個人而言，我放棄了代碼合同，直到它有機會再成熟一些。語法很尷尬（我們確實需要一個簡單的表示，特別是不可爲空的參數），並且您可以經歷大量的旋轉，試圖使複雜的系統靜態證明。不過，這是一個非常好的主意，我認爲只有在適當的合同支持複雜的靜態分析被納入.NET（實際的CIL元數據），C＃中的本地語言支持，而不是作爲一個尷尬的擴展。

另外一個問題是，我認爲從上到下包括私人和公共方法在內的小型應用程序合同申請過程非常有價值。當你完成所有事情證明的過程時，它揭示了很多你每天都沒有意識到的隱含假設。您還經常發現您從未考慮過的失敗案例，因爲您在設計合同時培養的思維模式凸顯了您做出假設的要點，並鼓勵您考慮是否有時會違反您的假設。我沒有時間在日常工作上做這個工作，但是我從測試代碼合同的那段時間開始學到了很多東西。

Answer 2

合同通常只在公共方法之前/之後進行檢查。私有方法只作爲調用公共方法的一部分被調用，所以不需要單獨檢查。

http://en.wikipedia.org/wiki/Class_invariant