譯自 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）指總為真的條件或者說斷言。即該方法告訴使用者：“如果它在呼叫我之前為真，那麼我可以保證在我呼叫結束後它仍然為真”。不變式是前置條件和後置條件的組合。在呼叫方法之前和之後，它都必定為真。

總結

通過本文，我們瞭解了什麼是“前置條件”和“後置條件”。我們看到前置條件即在呼叫方法之前必須為真的條件，而後置條件即在方法呼叫結束後必定為真的條件。