先決條件

在計算機編程中，先決條件或先驗條件指在執行一段代碼前必須成立的條件。

基本介紹

• 中文名：先決條件
• 領域：計算機

簡介

如果先決條件被違反了，則代碼將產生未定義行為，因此其預期的工作能否履行也是未知的。不正確的先決條件還可能引發安全問題。

通常，先決條件包括在關於這段代碼的文檔中。有時它可通過特定的語法結構（如警衛或斷言）在代碼中進行檢測。

例如，階乘只定義於自然數（大於等於零的整數）。因此計算階乘的程式將會假定輸入的值是一個整數，並且它大於等於零，這就是一個先決條件。

在面向對象編程中

面向對象編程中先決條件是契約式設計的一個重要組成部分。契約式設計還包括後置條件和不變條件的概念。

要成功執行一個子程式所需的任何關於對象狀態的限制條件都定義在先決條件中。從程式開發者的角度來看，這就構成了契約中子程式調用者的一部分。調用者有義務來確保在調用子程式前滿足先決條件，而被調用的子程式則以後置條件來反饋給調用者。

先決條件與繼承

在繼承的關係中，繼承了子程式的子類必須滿足先決條件。也就是說對被繼承的子程式的任何實現或重新定義，也必須遵守他們所繼承的契約。重新定義的子程式可以削弱先決條件，但不能增強。

不變條件

在計算機科學中，不變條件是指，在程式執行過程或部分過程中，可始終被假定成立的條件。比如，循環不變條件是指在循環開始和結束後始終成立的條件。

不變條件在邏輯推理電腦程式正確性時，特別有用。最佳化編譯器理論、契約式設計設計方法論及形式方法，都十分依賴於電腦程式的不變條件。

程式設計師往往使用斷言來現式定義不變條件。一些面向對象程式語言也有特定語法定義類不變條件。

契約式設計

契約式設計（英語：Design by Contract，縮寫為 DbC），一種設計計算機軟體的方法。這種方法要求軟體設計者為軟體組件定義正式的，精確的並且可驗證的接口，這樣，為傳統的抽象數據類型又增加了先驗條件、後驗條件和不變式。這種方法的名字里用到的“契約”或者說“契約”是一種比喻，因為它和商業契約的情況有點類似。

因為Design by Contract是屬於Eiffel Software的註冊商標，很多開發人員用契約式編程（Programming by Contract），契約編程（Contract Programming），或者契約優先式開發（Contract-First development）來指代這種方法。微軟也採用這種設計方法，稱為代碼契約（Code Contracts）。