循环不变性

循环不变性（loop invariants）不只是一种计算机科学的思想，准确地说是一种数学思想。在数学上阐述了通过循环（迭代、递归）去计算一个累计的目标值的正确性。

比如插入排序，每次循环从数组A中取出第j个元素插入有序区A[1 .. j-1]，然后递增j。这样A[1 .. j-1]的有序性始终得到保持，这就是所谓的“循环不变”了。

循环不变式主体是不变式，也就是一种描述规则的表达式。其过程分三个部分：初始，保持，终止。
　　1、初始：保证在初始的时候不变式为真。
　　2、保持：保证在每次循环开始和结束的时候不变式都为真。
　　3、终止：如果程序可以在某种条件下终止，那么在终止的时候，就可以得到自己想要的正确结果。
　　在这三个部分中，前两个是条件，最有一个是结论。

利用循环不变式(loop invariant)来证明循环的正确性与用数学归纳法(induction)证明数学等式的相同点在于：

都需要验证初值，或初始状态是否满足条件。
之后再证明在归纳或递推的过程中仍然满足这种条件。（这个条件在数学归纳中叫做递推关系，在循环中就是循环不变式(loop invariant)）。

循环不变式(loop invariant)与数学归纳法(induction)的区别在于：

数学归纳可能是无限的，是无限地腿的，但循环不变式所要证明的循环是要结束并给出正确结果的。

如何找循环不变式？

由于算法是一步步执行的，那么如果每一步（包括初试和结束）都满足一个共同的条件，那么这个条件就是要找的循环不变性（loop invariant）。

（编辑：李大同）

【声明】本站内容均来自网络，其相关言论仅代表作者个人观点，不代表本站立场。若无意侵犯到您的权利，请及时与联系站长删除相关内容!