循环不变量

循环不变量（loop invariant）是一个不变量，被用来证明循环的特点，更多地，算法使用循环 (usually 正确性)。非正式的说，一个循环不变量是指在循环开始和循环中每一次迭代时永远为真的量，这意味着在循环中和循环结束时循环不变量和循环终止条件必须同时成立。

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

霍尔逻辑在弗洛伊德-霍尔逻辑，While循环的部分正确性被下列的规则所确定：

意思是：

一个 while 循环不可以使得 为假 - 如果在给定条件 下循环体 body 不会使不变量从真变成假，则 将在循环之后如在循环之前一样为真。

只要 为真时必会循环。若其于循环之后中止，则当为假。1

循环不变代码外提循环不变代码外提（英语：loop-invariant code motion，缩写LICM）在计算机编程中是指将循环不变的语句或表达式移到循环体之外，而不改变程序的语义。循环不变代码外提在英文中又被称为hoisting或scalar promotion，是编译器中常见的优化方法。1

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

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

递归递归（英语：Recursion），又译为递回，在数学与计算机科学中，是指在函数的定义中使用函数自身的方法。递归一词还较常用于描述以自相似方法重复事物的过程。例如，当两面镜子相互之间近似平行时，镜中嵌套的图像是以无限递归的形式出现的。也可以理解为自我复制的过程。

归经常被用于解决计算机科学的问题。在一些编程语言（如Scheme、Haskell中），递归是进行循环的一种方法。2

本词条内容贡献者为:

王沛 - 副教授、副研究员 - 中国科学院工程热物理研究所