譯自 Preconditions and Postconditions
在這篇文章中,我們將討論術語前置條件(Precondition)和后置條件(Postcondition)。
前言
“前置條件”和“后置條件”這兩個詞看起來很嚇人,但理解起來並不復雜。
定義
首先,讓我們以一種正式的方式來定義“前置條件”和“后置條件”這兩個詞。
前置條件
前置條件是在方法運行之前必須為真的條件(condition)或者說斷言(predicate)。換句話說,該方法告訴使用者:“這是我對你的期望”。即正在調用的方法期望在調用該方法之前或調用該方法時滿足一定的條件。除非滿足前置條件,否則不能保證操作會按其應有的方式執行。
后置條件
后置條件是在方法運行之后能夠被保證為真的條件或者說斷言。換句話說,該方法告訴使用者:“這是我承諾為你做的”。如果操作正確且滿足前置條件(可能有多個),則可以保證后置條件為真。
現實世界中的例子
讓我們看看在現實世界中,什么是前置條件和后置條件。
- 吃掉披薩——前置條件:有一個披薩;后置條件:披薩沒了。
- 從 ATM 的借記帳戶中取款——前置條件(有多個):首先,提取的金額應小於等於該帳戶中剩余的金額,其次,提取的金額應小於等於 ATM 中剩余的金額;后置條件:ATM 和帳戶上的余額提醒應等於其原始金額減去提取金額。
- 馬里奧擊敗鮑澤——前置條件:鮑澤出現;后置條件:馬里奧救了皮奇。
一個更具體的例子
現在來看一個更具體的例子。假設我們有一個用於計算平方根的函數,那么這里的前置條件即傳給這個平方根函數的參數必須為非負數,后置條件即計算得到的結果的平方必定與傳入的參數相等。可將其表示為:
def square_root(x):
assert x >= 0 // _前置條件_
計算過程...返回一個名為 Y 的值
assert y*y == x // _后置條件_
return y
編程實例
假設我們有這樣一個函數:
int getSum(int a, int b)
{
int sum = a + b;
return sum;
}
這個函數的功能是計算給定的兩個整數的和並將和返回。對該函數來說,前置條件為給定的兩個值都為整數,后置條件為這兩個整數的和被返回。
不變式
我們有時會看到“不變式”一詞,不變式(invariant)指總為真的條件或者說斷言。即該方法告訴使用者:“如果它在調用我之前為真,那么我可以保證在我調用結束后它仍然為真”。不變式是前置條件和后置條件的組合。在調用方法之前和之后,它都必定為真。
總結
通過本文,我們了解了什么是“前置條件”和“后置條件”。我們看到前置條件即在調用方法之前必須為真的條件,而后置條件即在方法調用結束后必定為真的條件。