「它通過了」的麻煩
你寫了一個小演算法——比方說，找出清單裡最大的數。你餵給它幾個清單，盯著答案看，全都看起來對。完成了？很容易就說是。但停下來想想你究竟檢查了什麼：你確認了這個方法在你「碰巧」試的那些「特定」輸入上給出正確答案。我們真正在意的問題卻不同、也大得多：它在「每一個」有效輸入上都給出正確答案嗎？這道鴻溝——介於「在我試過的上面有效」與「在所有東西上有效」之間——正是本階存在的全部理由。
麻煩出在算術。一個 20 個小整數的清單已經有天文數字般多的可能；一個接受任意長度輸入的方法則有「無窮」多種。再大的有限測試堆，都蓋不住無窮的輸入空間。所以一套測試永遠只能做兩件事之一：抓到一個臭蟲，或抓不到。它能證明你的演算法錯了（一個失敗的案例就夠），卻永遠無法證明它對了。這個不對稱是本階最重要的單一觀念，也正是要正確性，而非看似合理這個說法所捕捉的。
證明給你的、測試給不了的
一個正確性論證是一段一次涵蓋「所有」輸入、而非逐一處理的推理。你不是在第 1 筆輸入、再第 2 筆、再第 3 筆上跑演算法，而是去推理演算法本身的結構——它的迴圈、它的遞迴、它維持的關係——並證明無論輸入是什麼，它回傳的答案都必須滿足問題的要求。一個仔細的論證，就退役了整套無窮的測試。這正是我們所說的演算法正確性：不是「我還沒找到反例」，而是「沒有反例，理由如下」。
用物理來想這個差別。測試像是開幾輛卡車過橋、看它沒垮，藉此檢查橋撐得住。證明則像是結構計算，顯示橋對「每一個」直到額定上限的載重都撐得住——包括還沒有人開上去的載重。計算不取代卡車（你還是要測試！），但只有計算能讓你對你從未試過的載重說出真話。在程式裡，「你從未試過的載重」就是明年才會到來的輸入，來自你還沒見過的使用者，以你想不到的組合出現。
正確演算法的兩半
當我們說一個演算法是正確的，其實悄悄做了兩個分開的承諾，把它們拆開來看很值得。第一個是：「如果」演算法停下來，它產生的答案是對的。第二個是：它真的「會」停下來——絕不會永遠跑下去。光是第一個承諾稱為部分正確性；兩個承諾合在一起則是完全正確性。這個區分就是部分正確性與完全正確性這個說法，而把兩者搞混是一個經典的錯誤。
為何要費事拆開？因為它們是用「完全不同的工具」來證明的，而你在本階稍後會遇到這兩者。「答案正確」這一半，是靠迴圈不變量（一個在每一趟都保持為真的性質）並以數學歸納法支撐來確立的。「它會停」這一半則需要另一段論證：你找出某個在每一步都嚴格遞減、又不可能永遠遞減下去的量——這就是透過遞減度量達成的終止性。一個演算法可以是部分正確的，卻在某些輸入上永遠迴圈；那仍是臭蟲，只是另一種，而只有終止性論證才抓得到它。
標好球門：前置與後置條件
在你能證明一個演算法「正確」之前，你得先釘死它的正確「意味著什麼」——否則這個詞會憑空飄著。我們用兩個敘述來做這件事。前置條件說明呼叫者承諾交進來什麼（「輸入是一個整數清單」、「陣列已經排好序」、「n 至少是 1」）。後置條件說明若那個輸入被遵守，演算法承諾交出什麼（「輸出是最大的元素」、「陣列排好序回來」）。兩者合起來就構成前置條件與後置條件所命名的那份契約。
這份契約不是繁文縟節——它是讓一個正確性宣稱「可被檢查」的關鍵。「二分搜尋是正確的」在你加上前置條件「陣列已排序」之前毫無意義。餵給二分搜尋一個未排序的陣列，它可能回傳垃圾；那不是二分搜尋的臭蟲，因為是呼叫者破壞了契約。陳明前置條件，精準地告訴你你對哪些輸入欠一個正確答案、又有權忽略哪些。本階的每個證明都會悄悄地以「假設前置條件」開始，並以「確立後置條件」結束。
{ precondition } <-- what we may assume about the input
ALGORITHM
{ postcondition } <-- what we must guarantee about the output
PROVE: precondition ==> algorithm halts AND postcondition holds直覺對你撒謊的地方
如果測試證明不了正確性，你或許會盼望一個自信的揮手就能——「看一眼嘛，顯然有效」。有時這直覺是對的。但它常常正是臭蟲藏身之處，因為看似合理的推理會跳過那個會壞掉的案例。想想一個靠反覆對半切範圍來找項目的程序：它「感覺」顯然正確，然而邊界算術（範圍含不含兩端？要走到 `mid` 還是 `mid+1`？）是出了名地容易出微妙的錯，在少數輸入上永遠迴圈或漏掉目標。「在局部看起來沒問題」不是證明——這個主題你在貪婪演算法上會再見到，那裡一個局部最佳的選擇可能無法是全域最佳。
也要注意，連「通常沒問題」這種「統計式」的感覺都是錯誤的目標。一個演算法的行為取決於你給它哪個輸入，而最壞、最佳與平均情況可能天差地別。一個在 99.9% 的輸入上正確、在其餘悄悄出錯的方法，不是一個正確的演算法——它是一個難找的臭蟲。正確性是一個「對所有輸入」的宣稱，長尾裡藏不了例外。這正是為什麼我們拿「它通常有效」的舒適，去換證明這種更難、卻更堅固的貨幣。
- 陳明契約：寫下前置條件（你假設什麼）與後置條件（你必須保證什麼）。
- 證明部分正確性：找出一個迴圈不變量，並用歸納法證明，只要演算法停下來、後置條件就成立。
- 證明終止性：給出一個每一步嚴格遞減、又不可能永遠下降的度量，使演算法必定停止。
- 推得完全正確性：部分正確性加上終止性，合起來就表示演算法總會停下並給出正確答案。
那為什麼還要測試？
這一切都不意味著「停止測試」——測試與證明是夥伴，不是對手。測試抓得到證明抓不到的東西：一個打錯的字、紙上演算法與機器上程式碼之間的不一致、一個讀錯的函式庫、一個現實世界悄悄違反的前置條件。證明推理的是一個理想化的演算法；測試檢查的是它那一團混亂的實作。多數時候你會先伸手去拿測試，因為它快又便宜，而把完整的證明留給那承重的核心——在那裡一個隱藏的錯誤會是災難性的。
正確的心態是讓每種方法做它擅長的事。證明給你那個普遍的保證——「憑推理，對所有輸入為真」——這是再多測試都永遠提供不了的。測試給你一個對照現實的檢查，去對照你的推理與你正在跑的程式碼之間的落差。本階其餘部分會建起這份夥伴關係中「證明」的那一半，一次一個工具：先是迴圈不變量，再是歸納法，再是終止性，最後是兩個你可以模仿的完整實作證明。到最後，「我論證了它，論證在此」會變得和「我跑了它，看起來對」一樣自然。