循环不变式

循环不变式式证明算法正确性的一个重要方法，本篇文章将记录一下循环不变式。

百科里给循环不变式的定义为“每次循环体执行前后均为真的谓词”。最为关键的是找到合适的“断言”。

要通过这个证明算法的正确性，需要证明三点：

• 初始化：循环的第一次迭代开始前，断言为真。
• 保持：类似于数学归纳法的第二步，循环的某次迭代之前断言为真，那么循环迭代之后，断言仍为真。
• 终止：循环终止时，得到的结果就是自己想要的结果。

下面通过一个常见的例子来说明循环不变式：

int sum(int a[], int size)
{
    int i = 0;
    int sum = 0;
    while(i<size)
    {
        sum = sum + a[i];
        i = i + 1;
	}
    return sum;
}

这是一个十分简答的求和运算，不难得出“sum = 前k个数的和”，这便是断言，下面说明一下断言的正确性。

int sum(int a[], int size)
{
    int i = 0;
    int sum = 0;
    // M(k) = 0, 此时k = 0，所以初始化成立。
    while(i<size)
    {
        sum = sum + a[i];
        // M(k + 1) = 前 k + 1个数的和 = M(k) + a[k]
        i = i + 1;
        //转换之后，M(k) = 前k个数的和
	}
    return sum; //推出循环时，i == size，所以会有sum = 前size项的和，算法正确
}

能用循环不变式验证的算法还有很多的，以后慢慢体会。