循环不变量

维基百科,自由的百科全书
跳转至: 导航搜索

计算机科学中,循环不变量loop invariant),或“循环不变性”,是一组在循环体内、每次迭代均保持为真的性质,通常被用来证明算法循环的正确性。非正式的说,一个循环不变量是指在循环开始和循环中每一次迭代时永远为真的量,这意味着在循环中和循环结束时循环不变量和循环终止条件必须同时成立。

由于循环和递归的程序相似的原因,证明带有不变量的循环的部分正确性和证明通过归纳的递归程序的正确性极其相似。事实上,循环不变量通常是一个递归程序可以等价为一个给定循环的递归的属性。

霍尔逻辑[编辑]

弗洛伊德-霍尔逻辑[1][2]While循环部分正确性被下列的规则所确定:

\frac{\{C\land I\}\;\mathrm{body}\;\{I\}} {\{I\}\;\mathbf{while}\ (C)\ \mathrm{body}\;\{\lnot C\land I\}}

意思是:

  • 一个 while 循环不可以使得 I 为假 - 如果在给定条件 C 下循环体 body 不會使不变量 I 从真变成假,则 I 将在循环之后如在循环之前一样为真。
  • 只要 C 為真時 while(C)... 必會循環。若其於循環之後中止,則 C 當為假。

参考文献[编辑]

  1. ^ R. W. Floyd. "Assigning meanings to programs." Proceedings of the American Mathematical Society Symposia on Applied Mathematics. Vol. 19, pp. 19–31. 1967. ([1])
  2. ^ C. A. R. Hoare. "An axiomatic basis for computer programming". Communications of the ACM, 12(10):576–585, October 1969. doi:10.1145/363235.363259