插入排序——对于少量元素的排序，它是一个有效的算法。伪代码如下：
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]中的元素组成但是已将排序。因此算法正确。
原文：http://www.cnblogs.com/Wan-notes/p/6846444.html