2. 算法基础

循环不等式与插入排序的正确性

循环不变式：把A[1...j-1]的这些性质形式表示为循环不变式。

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

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

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

终止：在循环终止时，循环不等式仍为真。

对于插入排序，看看如何证明这些性质成立：

初始化：首先证明第一次循环迭代之前(j=2时)，循环不变式成立。子数组A[1..j-1]仅由单个元素A[1]组成，实际上就是A[1]中原来的元素。而且该数组是排序好的。表明第一次循环迭代之前循环不变式成立。

保持：内部for循环将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]中的元素组成，但已排好序。