循环不变量

在计算机科学中，循环不变量是程序循环的一个属性，在每次迭代之前（和之后）都是真的。它是一个逻辑断言，有时在代码中通过断言调用来检查。知道它的不变量对于理解一个循环的效果是至关重要的。

在形式化程序验证中，特别是Floyd-Hoare方法，循环不变量由形式化谓词逻辑表达，并用于证明循环的属性和采用循环的扩展算法（通常是正确性属性）。

循环不变量在进入循环和每次迭代之后都是真的，因此在退出循环时，循环不变量和循环终止条件都可以得到保证。从编程方法论的角度来看，循环不变式可以被看作是循环的一个更抽象的规范，它表征了循环的更深层次的目的，超越了这个实现的细节。

一篇调查文章涵盖了计算机科学许多领域的基本算法（搜索、排序、优化、算术等），从其不变量的角度来表征每一个算法。

由于循环和递归程序的相似性，用不变量证明循环的部分正确性与通过归纳证明递归程序的正确性非常相似。事实上，循环不变量往往与与给定循环等价的递归程序所要证明的归纳假设相同。

下面的C语言子程序max()返回其参数数组a[]中的xxx值，条件是其长度n至少为1。在第3、6、9、11和13行提供了注释。每个注释都对函数的那个阶段的一个或多个变量的值做了断言。

在循环体内，在循环的开始和结束（第6行和第11行），突出显示的断言是完全一样的。当到达第13行时，这个不变量仍然成立，而且我们知道第5行的循环条件i!=n已经变成了假的。

这两个属性共同意味着m等于a[0...n-1]中的xxx值，也就是说，从第14行返回的是正确的值。intmax(intn,constinta[]){intm=a[0];//m等于a[0...0]中的xxx值inti=1;while(i!=n){//m等于a[0...i-1]if(m<a[i])m=a[i];//m等于a[0...i]的xxx值++i;//m等于a[0...i-1]的xxx值}//m等于a[0...i-1]的xxx值，且i=nreturnm;}按照防御性编程范式，第5行的循环条件i!=nxxx修改为i<n，以避免n的非法负值的无尽循环。

虽然这种代码上的改变从直觉上来说不应该有什么不同，但导致其正确性的推理变得有些复杂，因为在第13行只有i>=n是已知的。为了得到i<=n也成立，这个条件必须包含在循环不变量中。

很容易看出，i<=n也是一个循环的不变量，因为第6行的i<n可以从第5行的（修改过的）循环条件中得到，因此在第10行的i被递增后，第11行的i<=n也成立。然而，当循环不变量必须手动提供给形式化程序验证时，像i<=n这样直观的太明显的属性常常被忽略。

在Floyd-Hoare逻辑中，while循环的部分正确性受以下推理规则的制约。

如果某些属性I是由代码body保留的{displaystyle{mathrm{body}}这意味着：如果某个属性I被代码body保留了，那么它就会被保留。}-更确切地说，如果I在执行body之后保持不变body{displaystyle{mathrm{body}}--更确切地说，如果I在执行body之后仍然成立，那么，body就会被保留。

}只要C和I在之前都成立--（上线），那么在整个循环执行后，C和I被保证分别为假和真，即(C)body{displaystyle{mathtt{while}}(C)mathrm{body}}}，只要我在循环之前是真的（下行）。换句话说。上面的规则是一个演绎步骤，它的前提是Hoare三联体{C∧I}body{I}{displaystyle{ClandI};mathrm{body};{I}}.;{I}}.这个三联体实际上是一个关于机器状态的关系。

只要从一个布尔表达式的状态开始，它就会成立C∧I{displaystyleClandI}为真，并成功地执行一些叫做"I"的代码。为真，并且成功地执行了一些叫做body{displaystylemathrm{body}的代码。}，机器最终处于一个I为真的状态。

如果这个关系可以被证明，那么这个规则就可以让我们得出结论，成功执行程序的while(C)body{displaystyle{mathtt{while}}(C)mathrm{body}的成功执行。}将导致从一个I是真的状态，到一个I是真的状态。