插入排序算法類似於玩撲克時抓牌的過程，玩家每拿到一張牌都要插入到手中已有的牌裡，使之從小到大排好序。例如（該圖出自[算法導論]）：
也許你沒有意識到，但其實你的思考過程是這樣的：現在抓到一張7，把它和手裡的牌從右到左依次比較，7比10小，應該再往左插，7比5大，好，就插這裡。為什麼比較了10和5就可以確定7的位置？為什麼不用再比較左邊的4和2呢？因為這裡有一個重要的前提：手裡的牌已經是排好序的。現在我插了7之後，手裡的牌仍然是排好序的，下次再抓到的牌還可以用這個方法插入。
編程對一個數組進行插入排序也是同樣道理，但和插入撲克牌有一點不同，不可能在兩個相鄰的存儲單元之間再插入一個單元，因此要將插入點之後的數據依次往後移動一個單元。排序算法如下：
例 11.1. 插入排序
#include <stdio.h>
#define LEN 5
int a[LEN] = { 10, 5, 2, 4, 7 };
void insertion_sort(void)
{
int i, j, key;
for (j = 1; j < LEN; j++) {
printf("%d, %d, %d, %d, %d\n",
a[0], a[1], a[2], a[3], a[4]);
key = a[j];
i = j - 1;
while (i >= 0 && a[i] > key) {
a[i+1] = a[i];
i--;
}
a[i+1] = key;
}
printf("%d, %d, %d, %d, %d\n",
a[0], a[1], a[2], a[3], a[4]);
}
int main(void)
{
insertion_sort();
return 0;
}為了更清楚地觀察排序過程，我們在每次循環開頭插了打印語句，在排序結束後也插了打印語句。程序運行結果是：
10, 5, 2, 4, 7 5, 10, 2, 4, 7 2, 5, 10, 4, 7 2, 4, 5, 10, 7 2, 4, 5, 7, 10
如何嚴格證明這個算法是正確的？換句話說，只要反覆執行該算法的for循環體，執行LEN-1次，就一定能把數組a排好序，而不管數組a的原始數據是什麼，如何證明這一點呢？我們可以借助Loop Invariant的概念和數學歸納法來理解循環結構的算法，假如某個判斷條件滿足以下三條準則，它就稱為Loop Invariant：
第一次執行循環體之前該判斷條件為真。
如果“第N-1次循環之後（或者說第N次循環之前）該判斷條件為真”這個前提可以成立，那麼就有辦法證明第N次循環之後該判斷條件仍為真。
如果在所有循環結束後該判斷條件為真，那麼就有辦法證明該算法正確地解決了問題。
只要我們找到這個Loop Invariant，就可以證明一個循環結構的算法是正確的。上述插入排序算法的Loop Invariant是這樣的判斷條件：第j次循環之前，子序列a[0..j-1]是排好序的。在上面的打印結果中，我把子序列a[0..j-1]加粗表示。下面我們驗證一下Loop Invariant的三條準則：
第一次執行循環之前，
j=1，子序列a[0..j-1]只有一個元素a[0]，只有一個元素的序列顯然是排好序的。第
j次循環之前，如果“子序列a[0..j-1]是排好序的”這個前提成立，現在要把key=a[j]插進去，按照該算法的步驟，把a[j-1]、a[j-2]、a[j-3]等等比key大的元素都依次往後移一個，直到找到合適的位置給key插入，就能證明循環結束時子序列a[0..j]是排好序的。就像插撲克牌一樣，“手中已有的牌是排好序的”這個前提很重要，如果沒有這個前提，就不能證明再插一張牌之後也是排好序的。當循環結束時，
j=LEN，如果“子序列a[0..j-1]是排好序的”這個前提成立，那就是說a[0..LEN-1]是排好序的，也就是說整個數組a的LEN個元素都排好序了。
可見，有了這三條，就可以用數學歸納法證明這個循環是正確的。這和第 3 節 “遞歸”證明遞歸程序正確性的思想是一致的，這裡的第一條就相當於遞歸的Base Case，第二條就相當於遞歸的遞推關係。這再次說明了遞歸和循環是等價的。