算法導論第二章中提出了一個概念－－“循環不變式”

那么，何為循環不變式

我的理解是：

“循環不變式是用于證明算法正確性的一種工具”

它應該怎么用呢

• 首先，對于任意的一種算法，我們需要找出其循環不變式
• 然后，需要證明循環不變式的三條性質

對于插入排序算法，它的證明是這樣的：

• 設下標j為目前正在排序的數字的索引，開始時j = 1（C++中索引從0開始，我們這里從第二個元素開始排，至于為什么，請往下讀）
• 循環不變式：“for循環每次開始時，A[0…j-1]是有序的”

接下來我們證明三條性質：

• 初始化 ：循環的第?次迭代之前，循環不變式為真
• 保持 ：如果循環的某次迭代之前循環不變式為真，那么下次迭代之前它仍為真
• 終止 ：終止時不變式要能做到符合結果（比如：完成排序）

證明：

1.初始化：顯然，j = 1時，A[0…j-1]就是A[0]，只有一個數字，當然是符合循環不變式的

2.保持：若 A[0..j-1] 有序，將 A[j] 插入后，A[0..j] 仍有序

3.終止：終止時，當 j = n 時，A[0..n] 整體有序，排序完成

因此你可以看到，事實上，循環不變式就是用來規范證明算法正確性的工具

如果你對數學歸納法比較熟的話，很容易發現其實循環不變式就是數學歸納法的一個變種

如何找循環不變式？

由于算法是一步步執行的，那么如果每一步（包括初試和結束）都滿足一個共同的條件，那么這個條件就是要找的循環不變式（loop invariant）

一個例子：

二分查找

不變式：若目標值存在，則必在子數組 A[l..r] 中

證明要點：

初始化：l=0, r=n-1，覆蓋整個數組

保持：根據中間值比較調整邊界，目標值仍在新區間內

終止：l > r 時子數組為空，目標不存在 → 返回 -1


我們發現，三條性質都符合我們的要求（初始化和保持滿足不變式、終止符合要求的結果），所以算法正確

循環不變式不只是理論工具——它強迫你在寫循環時明確“我試圖維護什么”。這種思維習慣能顯著減少代碼錯誤。

——《算法導論》核心思想

插入排序

算法原理：

插入排序與我們手動整理一副牌的過程類似（這里我們引用算法導論上的比喻）

(注意，目前為了易讀，我們討論升序排序，對于非升序，參考GitHub:《算法導論》筆記src/insertion_sort(插入排序).h中的注釋

想象一下：你現在右手放著一副亂序的牌，左手開始時什么都沒有
我們規定：右手的牌是無序的，左手始終有序
那么，我們現在從右手拿出一張牌，放到左手中
此時，你左手的牌仍然有序，因為此時只有一張牌，符合規定

接著，我們去拿下一張牌，這時有兩種情況：
1.當前的牌面>=左手牌面
2.當前的牌面<左手牌面
對于1，我們直接將牌放于左手的頂部即可
對于2，我們需要將牌放于左手第一張的下面

讓我們重復這個過程：
1.取出一張牌，我們記錄它的值為key
2.從左手的第一張開始，逐個比較(我們記為A[j])，直到key<=A[j]，執行3；
3.那么此時，A[j+1]就是key這個值在左手上的正確位置，我們令A[j+1]=key，
相當于把key插入到對應位置
4.執行1-3，直到整個數列有序

問題是，在計算機中，我們沒辦法執行插入這個操作，更具體的說，令A[j+1]=key時，會丟失A[j+1]的值

此時想想排牌時的操作：當我們找到合適位置時，我們會將它右側的所有牌右移一點，騰出一個空位來

那么在算法中，我們應該怎么辦呢？

很簡單，我們做一點點修改：

在上述的過程2中，如果我們發現key>A[j]，我們令A[j+1] = A[j]

可以試驗一下：
假設左手牌為：2，4
當前的key = 3
當前的j = 1（C++索引從0開始）
執行2:由于4>key，我們讓A[j+1] = A[j]，即A[2] = A[1]

那么，此時A[j]已經復制到了A[j+1]，我們無論怎么操作都不會丟失A[j]的數據，相當于騰出來了一個空位

繼續執行2: 此時的j = 0，A[j] = A[0] = 2<key，執行3

執行3: 此時，A[j+1]就是key在左手的正確位置，所以令A[j+1]=key，而此時的A[j+1]就是上一輪的A[j]（因為每次j都會-1）

而上一輪的A[j]已復制到上一輪的A[j+1]也就是當前的A[j+2]

所以我們可以直接令A[j+1]=key，不會丟失任何數據

只要我們持續這個操作，右手的所有牌最終都會正確地到達左手的正確位置

如何形式化的驗證算法正確性：

算法導論給我們提供了一個方法，類似數學歸納法--“循環不變式”

關于循環不變式的詳解：參考docs/循環不變式.md

我們來證明插入排序的循環不變式

如何找循環不變式？

由于算法是一步步執行的，那么如果每一步（包括初始和結束）都滿足一個共同的條件，那么這個條件就是要找的循環不變式（loop invariant）

顯然的，我們一直在試圖維護左手牌堆是有序的這個性質
那么，插入排序的循環不變式就是：循環中，A[0…j-1]是有序的

接下來，我們證明循環不變式的三條性質：

1.初始化：顯然，j = 1時，A[0…j-1]就是A[0]，只有一個數字（這里我們提前將一張右手牌放入左手，并不影響結果），當然是符合循環不變式的
2.保持：若 A[0..j-1] 有序，將 A[j] 插入后，A[0..j] 仍有序
3.終止：終止時，當 j = n 時，A[0..n] 整體有序，排序完成

因此，插入排序最終被證明為正確的

關于代碼實現，參考GitHub:《算法導論》筆記src/insertion_sort(插入排序).h

P.S.在之后的算法設計文檔中，我們都使用循環不變式來設計和證明算法
文章及代碼已同步到GitHub：《算法導論》筆記，歡迎參考
如有錯誤，請不吝賜教