插入排序——对于少量元素的排序，它是一个有效的算法。伪代码如下：

　　INSERTION-SORT(A)

　　　　for j=2 to A.length

　　　　　　key=A[j]

　　　　　　i=j-1

　　　　　　while i>0 and A[i]>key

　　　　　　　　A[i+1]=A[i]

　　　　　　　　i=i-1

　　　　　　A[i+1]=key

在for循环每次迭代的开始，包含元素A[1..j-1]的子数组代表已经排序好的序列，而剩余数组A[j+1..n]代表仍未排序的元素。

循环不变式——具有像A[1..j-1]那样原来位于1到j-1的元素现在已经按序排列的性质。

关于循环不变式必须证明三条性质：

　　初始化：循环的第一次迭代之前，它为真。

　　保持：如果循环的某次迭代之前为真，那么下次迭代之前它仍为真。

　　终止：在循环终止时，不变式为我们提供一个有用的性质，该性质有助于证明算法是正确的。

类似于数学归纳法。

证明插入排序：

　　初始化：当j=2时，A[1..j-1]只有一个元素A[1]，实际上就是A[1]中原来的元素。因此，第一次循环迭代之前循环不变式成立。

　　保持：while循环将A[j-1]、A[j-2]、A[j-3]等向右移动一个单位，直到找到A[j]合适的位置，然后将A[j]插入该位置。此时A[1..j]由原来的A[1..j]中的元素组成，但是已经排序了。所以下一次迭代开始之前循环不变式成立。

　　终止：for循环终止条件是j>A.length=n。因为每次循环迭代j加1，那么必有j=n+1。在循环不变式中将j用n+1代替。我们有：A[1..n]由原来A[1..n]中的元素组成但是已将排序。因此算法正确。

插入排序