不變量的終止步驟（termination step）

迴圈證明的前兩部分（初始化與維持）只告訴你不變量在每一輪都為真。它們本身並不能說明程式正確——只是讓一個承諾一直保持有效。終止步驟才是你收取回報之處：你取出迴圈離開時不變量的樣子，把它與迴圈離開的原因（離開條件）結合，讀出你真正想要的結論。

具體地說，迴圈之所以離開，是因為它的繼續條件不再成立；在那一刻你同時握有不變量（自始至終為真）與迴圈條件的否定。把兩者合取，通常就釘住了結果。以不變量「A[1..i-1] 已排序」的插入排序為例，迴圈在 i <= n 時繼續，故在 i = n+1 時離開；代入得「A[1..n] 已排序」，也就是整個陣列——完成。再看二分搜尋，不變量「若 x 在陣列中則它落在 [lo, hi] 內」加上離開條件「lo > hi」（窗口為空）便逼出「x 不在陣列中」，所以回傳「找不到」是正確的。

這裡藏著兩個警告。第一，這一步只關乎「假設迴圈會停」時結果的正確性；迴圈到底會不會停是另一個問題，由終止度量回答。所以不變量證明的「終止步驟」確立的是部分正確性；完全正確性還需要一個遞減的良基度量。第二，你必須誠實面對確切的離開值（是 i = n+1，不是 n）；把這個邊界弄錯，就是經典的差一錯誤，而一個誠實的終止步驟正好能抓到它。