在之前的一篇文章里写到算法的正确性的概念以及它的作用，下面就来写写循环不变量在算法的正确性证明中的用法。
循环不变量（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 中全部元素合并排序了， 从而证明了算法的正确性。
