在計算機編程中,後置條件指在執行一段代碼後必須成立的條件或謂詞。
例如,階乘的結果應該是大於等於1的整數。
物件導向編程中後置條件是契約式設計的一個重要組成部分。契約式設計還包括先決條件 和不變條件的概念。
被調用的子程序以後置條件來反饋給調用者。[1]
在繼承的關係中,繼承了子程序的子類必須滿足鍥約。子類中重新定義的子程序可以加強後置條件,但不能削弱。[2]