伪代码
Insertion-Sort(A)
for j = 2 to length[A]
do key ← A[j]
//insert A[j] to sorted sequence A[1, ..., j-1]
i ← j-1
while i > 0 and A[i] > key
do A[i+1] ← A[i]
i ← i-1
A[i+1] ← key
循环不变量
在每次循环的开始,子数组 A[1, …, j-1] 包含原来数组中 A[1, …, j-1] 但已经是有序的。
证明
初始化
初始化,令 j=2,A[1, …, j-1] = A[1, 1] = A[1],已经有序。
维护
每一层循环维护循环不变量。
终止
j=n+1,
A[1, …, j-1] = A[1, n] 是有序的。