「算法原理与实现」插入排序与循环不变式

1、循环不变式与插入排序的正确性

示例：对A = <5,2,4,6,1,4>进行插入排序

动图示例演示

上图表明A = <5,2,4,6,1,4> 进行插入排序的算法是如何工作的。下标j指出正被插入到手中的“当前元素”。在for循环（循环变量为j）的每次迭代的开始，包含元素A[1..j-1]的子数组构成了当前排序好的元素，剩余的子数组A[j + 1...n]对应于还未排序的元素。事实上，元素A[1...j-1]就是原来位置1到j-1的元素，但是现在已经按序排列。我们把A[1...j-1]的这些性质形式地表示为一个循环不变式。

循环不变式主要用来帮助我们理解算法的正确性。关于循环不变式，我们必须证明三条性质：

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

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

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

2、插入排序伪代码

InsertSort(A)
    for j = 2 to A.length
        key = A[j];
        // Insert A[j] into the sorted sequence A[1...j-1]
        i = j - 1;
        while i > 0 and A[i] > key
            A[i + 1] = A[i];
            i = i -1;
        A[i + 1] = key;

3、插入排序如何证明循环不变式成立？

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

保持：证明每次迭代保持循环不变式保持不变。非形式化，for循环体的4~7行将A[j-1]、A[j-2]、A[j-3]等向右移动一个位置，知道找到A[j]的适当位置，第8行将A[j]的值插入该位置。这是子数组A[1..j]由原来在A[1..j]中的元素组成，但已按顺序排列。那么对for循环的下一次迭代增加j将保持循环不变式。

终止：最后研究在循环终止时发生了什么。导致for循环终止的条件是 j > A.Length = n 。因此每次循环迭代j增加1，那么必有j = n + 1。在循环不变式的表述中将j用n+1代替，我们有：子数组A[1..n]由原来在A[1..n]中的元素组成,但已按序排列。此时，子数组A[1..n]就是真个数组，我们推断整个数组已排序。因此算法正确。