在之前的一篇文章里写到算法的正确性的概念以及它的作用,下面就来写写循环不变量在算法的正确性证明中的用法。
循环不变量(loop invariant)
在使用循环的算法里,可以通过循环不变量证明其正确性。
所谓循环不变量是指一种在整个循环过程中保持不变的性质,它必须在以下3种情况下均保持不变,且该性质在循环终止后能证明算法的正确性。
- 初始化(循环初始化后,循环条件测试前)
- 迭代(第 n 次迭代后,第 n+1 次迭代前)
- 结束(循环终止即循环条件判断为 false 时)
例子
接下来就归并排序(Merge sort)中的 merge 函数来说明一下循环不变量
1: int* merge(int* sld, int* srd, int lc, int rc)
2: {
3: int tc = lc + rc;
4: int* md = (int*) malloc(sizeof(int) * (tc));
5:
6: int li = 0; // 左数据当前元素索引
7: int ri = 0; // 右数据当前元素索引
8: for (int i = 0; i < tc; ++i)
9: {
10: if (li >= lc) //左数组数据已取完
11: md[i] = srd[ri++];
12: else if (ri >= rc) //右数组数据已取完
13: md[i] = sld[li++];
14: else if (sld[li] <= srd[ri]) //左右数据均未取完,取各自当前元素比较
15: md[i] = sld[li++];
16: else
17: md[i] = srd[ri++];
18: }
19:
20: return md;
21: }
先解释一下这个函数的作用,sld 和 srd 为已排序数组,大小分别为 lc 和 rc,循环 tc (lc + rc) 次把它们的元素进行比较并复制到新分配的数组 md 中,那要怎么证明这个算法的正确性呢。
让我们先设定循环不变量,然后看8-18行的循环能否在以上3种情况都满足这个循环不变量。
md[0-i) 中的元素为 sld[0-li) 和 srd[0-ri) 元素之和排序后的结果。
- 初始化
此时 i=0,li=0,ri=0,因此 md[0),sld[0),srd[0) 的大小均为0,满足循环不变量。 - 迭代
每次迭代都必须比较 sld[li] 和 srd[lr] 将较小的复制到 md[i] ,此时 md[0-i] 为 md[0-i) + min( sld[li], srd[ri] ),并将li 或 lr 增 1, 将 i 增 1 满足循环不变量。 - 结束
循环终止条件为 i>=tc (lc + rc) ,此时 md[0-tc) 中的元素为 sld[0-lc) 和 srd[0-rc) 元素之和排序后的结果。
结束时循环不变量给了我们一个有用信息,此时 md 已经把 sld 和 srd 中全部元素合并排序了, 从而证明了算法的正确性。