先決條件

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

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

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

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

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

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

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

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

程序員往往使用斷言來現式定義不變條件。一些面向對象編程語言也有特定語法定義類不變條件。 ^[1] 

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

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