[科普中国]-循环不变代码外提

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

在正式程序验证中，特别是Floyd-Hoare方法，循环不变量由形式谓词逻辑表示，并用于证明循环的属性和通过使用循环的扩展算法（通常是正确性属性）。 循环不变量在进入循环并且在每次迭代之后都是真的，因此在从循环退出时，可以保证循环不变量和循环终止条件。

非正式的例子下面的C子例程max（）返回其参数数组a []中的最大值，前提是它的长度n至少为1.注释在第3,6,9,11和13行提供。每个注释都有一个关于它的断言 函数该阶段的一个或多个变量的值。 循环体内，循环开始和结束时（第6行和第11行）的突出显示的断言完全相同。 因此，它们描述了循环的不变属性。 当到达第13行时，该不变量仍然成立，并且已知来自第5行的循环条件i！= n变为假。 两个属性一起暗示m等于[0 ... n-1]中的最大值，即，从第14行返回正确的值。

int max(int n,const int a[]) { int m = a[0]; // m equals the maximum value in a[0...0] int i = 1; while (i != n) { // m equals the maximum value in a[0...i-1] if (m