後置條件

在計算機編程中，後置條件指在執行一段代碼後必須成立的條件或謂詞。

例如，階乘的結果應該是大於等於1的整數。

在面向對象編程中

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

被調用的子程序以後置條件來反饋給調用者。^[1]

後置條件與繼承

在繼承的關係中，繼承了子程序的子類必須滿足鍥約。子類中重新定義的子程序可以加強後置條件，但不能削弱。^[2]

參見

• 契約式設計
• 衛語句
• 先決條件
• 霍爾邏輯
• 不變條件

參考資料

1. Meyer, Bertrand, Object-Oriented Software Construction, second edition, Prentice Hall, 1997, p. 342.
2. Meyer, 1997, pp. 570–573.