插入排序的不變量證明（insertion-sort invariant proof）

插入排序就是許多人整理一手撲克牌的方式：讓左手的牌保持排序好，拿起下一張牌，把它往左滑，直到它落在已排序牌中正確的位置。你已經整理好的那一疊每次增加一張，而且始終保持排序。把這份直覺變成證明，正是迴圈不變量的教科書範例，它在一個微小而具體的演算法上展示了全套機制（初始化、維持、終止）。

演算法：for i 從 2 到 n，取 key = A[i]，藉由把較大的元素右移，將它插入已排序的前綴 A[1..i-1]。迴圈不變量是：在索引 i 之每一輪開始時，子陣列 A[1..i-1] 由原本就在那裡的元素組成，且現在按排序順序排列。初始化：當 i = 2 時，A[1..1] 是單一元素，顯然已排序且未改動——不變量成立。維持：假設 A[1..i-1] 已排序；內層迴圈把每個大於 key 的元素右移一格，並把 key 放進空出的位置，於是之後 A[1..i] 已排序且含相同元素；i 遞增便為下一輪恢復了不變量。終止：迴圈在 i = n+1 時結束，故不變量讀作「A[1..n] 已排序且為原陣列的一個排列」——這正是後置條件。

這個證明是「為何不變量有效」的標準示範：三個部分每個都小而可檢驗，合起來卻能為每種規模、每種初始順序（包括重複值與已排序輸入）的陣列擔保結果。注意兩點誠實：第一，這論證的是正確性而非速度——插入排序在最壞情況下仍是 O(n^2)，儘管它正確。第二，不變量必須包含「為原陣列的一個排列」——移位從不創造或銷毀元素——否則證明就無法排除一個「把所有東西都覆寫成零」也算排序的程序。