關於設計的意見合同或代碼合同

Question

我目前正在閱讀了解更多關於設計的合同/代碼合同。

從我所知，它是寫合同（不變式，前置和後置條件），以確保代碼可以保持有序。它還將保證通過基於制衡的明確定義的機制來防止錯誤

但是這不會牽扯軟件性能嗎？由於每個方法調用之間都有額外的檢查。

我會非常感謝人們與我分享他們對Design By Contract的看法和經驗。缺點或優點是受歡迎的。

Answer 1

通常，這樣的框架支持運行時檢查和靜態分析。後者在編譯時（或之前）執行;它不會減慢你的代碼。前者可能會影響性能。

Microsoft Research Code Contracts項目就是一個很好的例子。您可以配置系統，使得：

• 靜態分析應用在編譯時可能執行合同的一個子集，甚至是在deigner環境;

• 爲調試模式下編譯的所有代碼啓用運行時檢查;和

• 爲發佈模式下編譯的代碼的公共API（非公共代碼沒有運行時檢查）啓用運行時檢查的子集。

這通常是性能和穩健性之間的良好折衷。

Answer 2

應用設計合同理念的一種方法是純靜態的。 考慮了功能max_element()合同：

/*@ 
requires IsValidRange(a, n); 
assigns \nothing; 
behavior empty: 
assumes n == 0; ensures \result == 0; 
behavior not_empty: 
assumes 0 < n; 
ensures 0 <= \result < n; 
ensures \forall integer i; 0 <= i < n ==> a[i] <= a[\result]; ensures \forall integer i; 0 <= i < \result ==> a[i] < a[\result]; 
complete behaviors; 
disjoint behaviors; 
*/ 
size_type max_element(const value_type* a, size_type n); 

如果你能確認在編譯時，一個實現始終保證在ensures條款後條件滿足前提是函數調用的參數滿足requires條款中的前提條件時，不必爲後置條件生成檢查。

同樣，如果您確認所有呼叫者在滿足其自己的先決條件時，只需使用滿足其先決條件的參數即可呼叫max_element()，那麼在函數輸入時不需要進行檢查。

以上示例來自ACSL by Example。該庫在ACSL中提供了許多功能合同。 C中的實現是爲合同提供的。這些實現已被靜態正式驗證以保證滿足前提條件的參數的所有調用的後置條件成立。因此，後期條件不需要運行時檢查。編譯器可以將註釋視爲註釋（它們是，使用/*@ ... */語法）。

Answer 3

按合同設計旨在確保正確實施 - 代碼正確寫入調用者和被調用者之間的預期API。理想情況下，您需要在開發和alpha測試環境中使用靜態分析工具和運行時檢查來驗證合同是否得到支持。希望那時你已經發現了任何有關API錯誤的實現錯誤。除非您嘗試追查錯誤，否則您可能不會使用運行時檢查測試版和生產。