循环不变量

计算机科学中,循环不变式(loop invariant,或循环不变量循环不变条件,也有译作循环不变性),是一组在循环体内、每次迭代均保持为真的性质(表达式),通常被用来证明程序伪码的正确性(有时但较少情况下用以证明算法的正确性)。简单说来,“循环不变式”是指在循环开始和循环中,每一次迭代时为真的性质。这意味着,一个正确的循环体,在循环结束时“循环不变式”和“循环终止条件”必须同时成立。

由于循环递归的相通,证明带有不变式的循环的部分正确性和证明通过归纳的递归程序的正确性极其相似。

循环不变代码外提(Loop-invariant code motion)是将循环内部不受循环影响的语句或表达式移到循环体之外,和此条目提到的循环不变式无关系。

霍尔逻辑

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

 

意思是:

  • while 循环不可以使得   为假 - 如果在给定条件   下循环体 body 不会使不变量   从真变成假,则   在循环之前一样为真,在循环之后也会为真。
  • 只要   为真时   必会循环。若其于循环之后中止,则   当为假。

参见

参考文献

  1. ^ R. W. Floyd. "Assigning meanings to programs." Proceedings of the American Mathematical Society Symposia on Applied Mathematics. Vol. 19, pp. 19–31. 1967. (存档副本 (PDF). 2008-12-09 [2009-11-10]. (原始内容 (PDF)存档于2008-12-09). )
  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