循环不变式

引言

　　算法程序形式化设计和证明是确保算法程序逻辑结构正确的最理想途径，是保证软件可靠性的有效手段之一；而体现了算法程序本质特征的循环不变式在 算法程序形式化方法中具有十分重要的作用。循环不变式是程序设计理论中的一个重要概念。这一概念的建立在程序设计从艺术走向科学这一历 史性的转变过程中起着巨大的推动作用，它不仅可以帮助人们理解那些难以理解的、精巧的循环算法程序，而且可以用来形式化地证明循环算法程序的正确性，也有 助于形式化地开发出高质量的循环程序 。

　　然而循环不变式的开发一直是算法程序设计领域中最具挑战性、最富有创造性的问题之一，许多计算机科学家和计箅机工作者也致力于这方面的研究。目前，人们把循环不变式定义为在循环的每次执行前后都为真的谓词 。

本文地址：http://www.cnblogs.com/archimedes/p/loop-invariant.html，转载请注明源地址。

定义

循环不变式：反映循环体中所有循环变量的变化规律并在循环体执行前后都为真的谓词称为该循环体的循环不变式 。

循环变量：在循环体中，其值随着循环体的执行不断发生变化的变量称为循环变量 。

算法导论第二章中的原文是：We state these properties of A[1 ‥ j -1] formally as a loop invariant。其中举的例子是插入排序，每次循环从数组A中取出第j个元素插入有序区A[1 .. j-1]，然后递增j。这样A[1 .. j-1]的有序性始终得到保持，这就是所谓的“循环不变 (loop invariant)”了。

这个概念主要用来检验算法的正确性。原文如下：

We use loop invariants to help us understand why an algorithm is correct. We must show three things about a loop invariant:

Initialization: It is true prior to the first iteration of the loop.

Maintenance: If it is true before an iteration of the loop, it remains true before the next iteration.

Termination: When the loop terminates, the invariant gives us a useful property that helps show that the algorithm is correct.

1. 初始化（循环第一次迭代之前）的时候，A[1 ‥ j -1]的“有序性”是成立的；

2. 在循环的每次迭代过程中，A[1 ‥ j -1]的“有序性”仍然保持；

3. 循环结束的时候，A[1 ‥ j -1]的“有序性”仍然成立。

编写循环时，找到让每次循环都成立的逻辑表达式很重要。这种逻辑表达式称为循环不变式（loop invariant）。循环不变式相当于用数学归纳法证明的“断言”。

循环不变式用于证明程序的正确性。在编写循环时，思考一下“这个循环的循环不变式是什么”就能减少错误。

举例应用

以一个非常简单的例子来讲解循环不变式吧。

代码清单是用C 语言写的sum 函数，功能是求出数组元素之和。参数array[] 是要求和的对象数组，size 是这个数组的元素数。调用sum 函数，会获得array[0] 至array[size-1] 的size 个元素之和。

代码清单--sum函数，求出数组的元素之和

int sum(int array[], int size)
{
    int k = 0;
    int s = 0;
    while(k < size) {
        s = s + array[k];
        k = k + 1;
    }
    return s;
}

在sum 函数中使用了简单的while 循环语句。我们从数学归纳法的角度来看这个循环，得出下述断言M(n)。这个断言就是循环不变式。

• 断言M (n ) ：数组array 的前n 个元素之和，等于变量s 的值。

我们在程序中成立的断言上标注注释，形成清单4-3 所示代码。

代码清单--在上面的代码中成立的断言上标注注释

在代码清单的第4 行，s 初始化为0。由此，第5 行的M(0) 成立。M(0) 即为“数组array 的前0 个元素之和等于变量s 的值”。这相当于数学归纳法的步骤1。

数学归纳法的步骤1（M(0)成立）

第7 行中，M(k) 成立。然后进行第8 行的处理， 将数组array[k] 的值加入s, 因此M(k+1) 成立。这相当于数学归纳法的步骤2。

数学归纳法的步骤2（M(k) M(k+1)成立）

请一定要理解第8 行，
s=s+array[k];

意为“在M(k) 成立的前提下，M(k+1) 成立”。

第10 行中k 递增1，所以第11 行的M(k) 成立。这里是为了下一步处理而设定变量k的值。

最后，第13 行的M(size) 成立。因为while 语句中的k 递增了1，而这时一直满足M(k), 走到第13 行时k 和size 的值相等。M(size) 成立说明sum 函数是没有问题的。因此，第14 行return 返回结果。

M (size )成立

综上所述，这个循环在k 从0 增加到size 的过程中一直保持循环不变式M(k) 成立。编写循环时，有两个注意点。一个是“达到目的”，还有一个是“适时结束循环”。循环不变式M(k) 就是为了确保“ 达到目的”。而k 从0 到size 递增确保了“适时结束循环”。

在下面的代码清单中，写明了M(k) 成立的同时k 递增的情形。（∧表示“并且”）

代码清单-- M (k )成立的同时k递增

 参考资料：

《算法导论》

《循环不变式开发新策略及其应用》