前置條件與後置條件（preconditions and postconditions）

在你能證明一個程式「正確」之前，你得先說清楚「正確」是什麼意思——而這取決於你被允許對輸入假設什麼、以及你對輸出欠下什麼。前置條件是呼叫者對輸入做的承諾（「陣列已排序」、「n >= 0」、「串列非空」）。後置條件是程序對給定輸入下之結果做的承諾（「回傳 x 的索引，若不存在則回傳 -1」；「陣列現已排序且為原陣列的一個排列」）。兩者合起來形成一份合約：假設前置條件，交付後置條件。

正確性永遠是相對於這份合約的。二分搜尋只有在「輸入陣列已排序」這個前置條件下才正確；對未排序的陣列執行它而得到「錯誤」答案，那不是演算法的錯——是呼叫者毀了合約。後置條件是你的不變量／歸納法證明在最後必須建立的；前置條件則是你在一開始有權假設的。對排序而言，一個嚴謹的後置條件有人們常忘的兩半：輸出必須已排序，而且必須是輸入的一個重排（排列）——一個輸出「一串排好序的零」的程序雖然「已排序」卻是錯的。

把這些條件寫下來，戰役就贏了一半，因為含糊的規格會藏住錯誤。它們也能組合：當一個程序呼叫另一個時，呼叫者必須確保被呼叫者的前置條件成立，然後便可倚賴被呼叫者的後置條件。這正是遞迴證明中合併步驟的運作方式——遞迴呼叫的後置條件，就是你據以推理的歸納假設。誠實的提醒：證明只擔保程式碼符合所陳述的後置條件；若後置條件本身沒能捕捉你真正要的東西，你可能有一個完美的證明，卻證錯了對象。