在之前的一篇文章里写到 算法的正确性 的概念以及它的作用，下面就来写写循环不变量在算法的正确性证明中的用法。

循环不变量（loop invariant）

在使用循环的算法里，可以通过循环不变量证明其正确性。
所谓循环不变量是指一种在整个循环过程中保持不变的性质，它必须在以下3种情况下均保持不变，且该性质在循环终止后能证明算法的正确性。

接下来就 归并排序（Merge sort） 中的 merge 函数来说明一下循环不变量

1: int* merge(int* sld, int* srd, int lc, int rc)
3:     int tc = lc + rc;
4:     int* md = (int*) malloc(sizeof(int) * (tc));
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:     }
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，满足循环不变量。