正确性的证明

循环不变式

观察插入排序算法的实现代码：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
int insertion_sort(int *array, const int LENGTH)
{
    int i, j, key;
    for (j = 1; j < LENGTH; j++){
    key = array[j];
    i = j - 1;
    while (i >= 0 && array[i] > key){
        array[i+1] = array[i];
        i--;
    }
    array[i+1] = key;
    }
    return 0;
}

如何严格证明这个算法是正确的？换句话说，只要反复执行该算法的for循环体，执行LENGTH-1次，就一定能把数组 array 排好序，而不管数组 array 的原始数据是什么，如何证明这一点呢？我们可以借助循环不变性（Loop Invariant）的概念和数学归纳法来理解循环结构的算法，假如某个判断条件满足以下三条准则，它就称为 Loop Invariant：

  • 初始化： 第一次执行循环体之前该判断条件为真。
  • 保持：如果“第N-1次循环之后（或者说第N次循环之前）该判断条件为真”这个前提可以成立，那么就有办法证明第N次循环之后该判断条件仍为真。
  • 终止：如果在所有循环结束后该判断条件为真，那么就有办法证明该算法正确地解决了问题。

只要我们找到这个循环不变式，就可以证明一个循环结构的算法是正确的。上述插入排序算法的循环不变式是这样的判断条件：第j次循环之前，子序列array[0…j-1]是排好序的。在上面的打印结果中，我把子序列array[0…j-1]加粗表示。下面我们验证一下循环不变式的三条准则：

  1. 第一次执行循环之前，j=1，子序列array[0…j-1]只有一个元素array[0]（你的左手只有一张牌），只有一个元素的序列显然是排好序的。
  2. 第j次循环之前，如果“子序列array[0…j-1]是排好序的”这个前提成立，现在要把key=array[j]插进去，按照该算法的步骤，把array[j-1]、array[j-2]、array[j-3]等等比key大的元素都依次往后移一个，直到找到合适的位置给key插入，就能证明循环结束时子序列array[0…j]是排好序的。就像插扑克牌一样，“手中已有的牌是排好序的”这个前提很重要，如果没有这个前提，就不能证明再插一张牌之后也是排好序的。
  3. 当循环结束时，j=LENGTH，如果“子序列array[0…j-1]是排好序的”这个前提成立，那就是说array[0…LENGTH-1]是排好序的，也就是说整个数组array的LENGTH个元素都排好序了。

剪贴法

用于证明最优子结构。

Comments

▲