把工具箱組裝起來
這一階已經交給你四件各自獨立的工具，而到目前為止，你都是分開認識它們的。從為什麼測試不是證明，你學到把演算法跑過幾個輸入，永遠只能顯示它做了什麼，卻無法顯示它必然會做什麼。從迴圈不變量，你拿到一個在迴圈每一輪都保持為真的敘述，並透過初始化、維持與終止時讀出結論來驗證它。從數學歸納法，你拿到驅動那個維持步驟的引擎。而從遞減度量，你拿到一種證明迴圈確實會停下來的方法。現在，我們在真實的程式碼上一次用上全部四件。
本文中每一個完整證明的骨架都是同一套，值得在細節登場之前先記在腦中。首先我們釘住一個前置條件（進場時我們假設什麼）與一個後置條件（離場時我們承諾什麼）。接著用一個迴圈不變量帶我們橫越整個迴圈，而在迴圈離開時讀出它，就交給我們後置條件——這就是部分正確性，也就是「若演算法停下來」的承諾。然後再用一個獨立的遞減度量，證明它確實會停。部分正確性加上終止性，等於完全正確性：它會停，而且停下來時答案是對的。
插入排序：先立好契約
插入排序一次一個元素地把已排序區擴大，做法就像你整理手中的撲克牌：你讓手裡已有的牌保持排好序，抽起下一張牌，然後把它往左滑過每一張比它大的牌，直到它落到自己的位置。以下就是我們要證明其正確性的虛擬碼，陣列 A 的索引從 1 到 n。
INSERTION-SORT(A, n):
for j = 2 to n: # outer loop
key = A[j]
i = j - 1
while i >= 1 and A[i] > key: # inner loop
A[i+1] = A[i]
i = i - 1
A[i+1] = key現在來訂契約。前置條件很寬鬆：A 是一個有 n 個可比較元素的陣列（任意順序）。後置條件才是「已排序」真正的意思，而我們必須把它講精確，否則無從證明：結束時，A[1] <= A[2] <= ... <= A[n]，而且最終陣列是原陣列的一個排列。後半這一句很要緊卻容易遺忘——一個把所有元素覆寫成零的演算法，會產生一個完美的非遞減陣列，卻把資料整個摧毀了。真正的排序必須是重新排列，而不是憑空捏造。
插入排序：不變量證明，以及它為何會停
整個證明繫於外層 for 迴圈一個精挑細選的迴圈不變量上。先用文字說一遍：在每一次以索引 j 開始的迭代之初，子陣列 A[1..j-1] 裝著的，正是原本坐在 A[1..j-1] 的那些元素，如今已排好序。這正是插入排序不變量。注意它把後置條件的兩半都包進去了——既已排序又是原本元素的一個排列——這樣當迴圈結束時，兩個承諾就一起掉出來。
- 初始化。在第一次迭代 j = 2 之前，區域 A[1..j-1] 就只是 A[1..1]，一個元素。單一元素必然是已排序的，也必然就是原本坐在那裡的同一個元素。迴圈還沒開始，不變量就已成立——基底情形不費吹灰之力。
- 維持。假設不變量在迭代 j 開始時成立：A[1..j-1] 是原元素的一個已排序排列。內層 while 迴圈把 key = A[j] 往左滑，逐一把較大的元素向右複製一格，並在遇到某個 <= key 的元素時（或滑出左邊界時）立刻停下。把 key 放進那個空隙，就是把它插入到恰好正確的名次，於是 A[1..j] 此刻已排序；又因為我們只搬動元素並重新安放 key，A[1..j] 仍是原本 A[1..j] 的一個排列。這正好就是下一次迭代 j+1 所需的不變量。
- 終止時讀出結論。for 迴圈在 j 剛好越過 n 時停下，也就是區域 A[1..j-1] 變成整個陣列 A[1..n] 時。把這代回不變量：A[1..n] 是原本 A[1..n] 的一個已排序排列。這逐字就是後置條件。部分正確性，搞定。
那個維持步驟還剩一個誠實的缺口：它悄悄假設了內層 while 迴圈會照我們說的去做、然後停下。內層迴圈欠它自己的子證明，而它有自己的小小不變量——「目前為止右移的元素全都 > key」——外加自己的遞減度量：索引 i 每一輪嚴格減 1，且下界為 0，所以它不可能永遠跑下去。真實的證明就是這樣巢狀的，迴圈裡套迴圈，各自承載自己的不變量；略過內層那個，正是排序證明暗中作弊最常見的一種方式。
不變量給了我們部分正確性——若插入排序停下，輸出就是已排序的。要升級成完全正確性，我們仍欠外層迴圈的終止性，而遞減度量論證能乾淨地解決它。把度量取為「還要跑的迭代次數」，也就是 n - j + 1。for 迴圈每一輪讓 j 恰好加一，所以這個度量每次嚴格遞減、且下界為零——一個非負整數又每一步嚴格遞減，不可能永遠這樣下去，所以外層迴圈必然終止。再結合內層迴圈自己的度量（索引 i 朝向 0 縮小），每一個迴圈都保證會停。把各塊縫起來：來自不變量的部分正確性，加上來自兩個遞減度量的終止性，得到完全正確性。插入排序總是會停，且只要它一停，陣列就是已排序的——這是證明出來的，不只是在我們碰巧試過的那些測試案例上觀察到的。
二分搜尋：同一道食譜，更鋒利的不變量
二分搜尋在一個已排序陣列 A[1..n] 中尋找目標 x，做法是反覆把視窗 [lo, hi] 對半砍。它的前置條件正是那個承重的關鍵——A 必須已排序，而整個證明重重地倚靠這一點。後置條件：若 x 存在，回傳一個滿足 A[i] = x 的索引 i，否則回報「不存在」。同一道四件工具的食譜照樣適用，只是不變量現在捕捉的是一個關於搜尋空間的主張，而非「已排序前綴」那種。
這就是二分搜尋不變量：如果 x 真的在 A 的某處，那麼它必落在目前的視窗 A[lo..hi] 之內。初始化立刻成立——我們從 lo = 1、hi = n 開始，視窗就是整個陣列，主張必然為真。維持步驟正是已排序這個前提賺到它身價的地方：把 x 與中點 A[mid] 比較。若 x < A[mid]，那麼因為 A 已排序，從 mid 往右的每個元素也都 > x，所以 x（若存在）不可能在那裡——我們安心地設 hi = mid - 1，不變量得以存活。對稱的情形則設 lo = mid + 1。我們從不丟掉那一半可能裝著 x 的視窗。
二分搜尋：讀出答案，以及它為何會停
終止時讀出結論這一步比插入排序更微妙，因為二分搜尋有兩種離開方式。若在某個中點 A[mid] = x，我們回傳 mid——完成，且答案正確，因為我們確實檢查過 A[mid] = x。否則迴圈在視窗清空、lo > hi 時結束。此時搬出不變量：它承諾過，若 x 在 A 中，它就會落在 [lo..hi] 之內。但 [lo..hi] 此刻是空的，所以 x 不可能在 A 中——我們正確地回報「不存在」。是不變量挑起了重擔：空視窗加上不變量，是一個關於「不存在」的證明，而不是一個猜測。
終止性再一次動用遞減度量，這裡的度量是視窗的大小，hi - lo + 1。每一次迭代，要嘛回傳（那就完成了），要嘛靠丟棄一個非空的半邊來嚴格縮小視窗，所以大小至少減一，且下界為零。因此它不可能永遠縮下去；迴圈必然停下。一個微妙的陷阱正好住在這裡：一個粗心的差一錯誤——比方說設成 hi = mid 而非 hi = mid - 1——可能在某一步讓視窗大小原封不動，度量沒能嚴格遞減，於是你得到一個無窮迴圈。正是遞減度量的證明，逼著你把那些更新寫得分毫不差。
退一步，欣賞這份對稱。兩個截然不同的演算法，一個在重排資料、一個在搜尋資料，卻都向同一套四步食譜俯首：寫出前置條件與後置條件，選一個把後置條件包在裡頭的不變量，證明「初始化—維持—終止」，再用一個遞減度量收尾成交。這正是歐幾里得最大公因數證明背後、以及你在這條學習階梯更高處會遇見的、遠為精巧的演算法之正確性論證背後，同一副骨架。這套技術可以放大；只有不變量的選擇會變得更聰明而已。
證明買到了什麼，又沒買到什麼
對於我們剛剛確立的東西，要誠實地交代它的範圍。我們證明了這兩個演算法正確——它們算出正確答案且會停。這是一個關於演算法在理想化機器模型上的敘述，對於成本則隻字未提。插入排序可被證明正確，最壞情況卻跑在 Theta(n^2)；二分搜尋可被證明正確，跑在 O(log n)。正確性與效率是兩個不同的問題，由不同的機制來回答——不變量告訴你答案是否正確，從不告訴你你多快抵達它。
還有兩條值得點名的邊界。其一，一個證明的好壞，取決於它的模型：我們假設整數比較花固定一步，且陣列讀取是精確的。真實機器有溢位、浮點捨入與有限記憶體；著名的二分搜尋溢位錯誤（mid = (lo + hi) / 2 在巨大陣列上溢位）是一個缺陷，但它不在數學裡，而在所假設的算術裡。正確性證明認證的是演算法本身，而一份忠實的實作是另一份獨立的責任。其二，我們的證明認證的是這個演算法符合這份規格——它對於規格本身是不是你真正想要的那份，什麼也沒說。垃圾的後置條件進去，垃圾的保證出來。
這些提醒沒有一條削弱了這套方法；它們只是磨利了你揮舞它的方式。一個迴圈不變量加上一個遞減度量，是人類所知最可靠的辦法，能讓我們確定一段程式碼確實做到它所宣稱的，橫跨那無窮多個測試永遠觸及不到的輸入。這一階學完，你就能讀一個陌生的演算法並問出對的問題——不變量是什麼、度量是什麼、前置條件在哪裡被消耗——而這個習慣，正是「相信一個演算法能用」與「知道它能用」之間的分界。