循环不变式

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

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个元素都排好序了。

剪贴法

用于证明最优子结构。