查看“︁循环不变量”︁的源代码

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

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

[[循环不变代码外提]]（Loop-invariant code motion）是將循环內部不受循環影響的語句或表達式移到循環體之外，和此條目提到的循环不变式無關係。

==霍尔逻辑==
在[[霍尔逻辑|弗洛伊德-霍尔逻辑]]，<ref>R. W. Floyd. "Assigning meanings to programs." Proceedings of the American Mathematical Society Symposia on Applied Mathematics. Vol. 19, pp. 19–31. 1967. ({{cite web |url=http://laser.cs.umass.edu/courses/cs521-621.Spr06/papers/Floyd.pdf |title=存档副本 |accessdate=2009-11-10 |date=2008-12-09 |deadurl=yes |archiveurl=https://web.archive.org/web/20081209122115/http://laser.cs.umass.edu/courses/cs521-621.Spr06/papers/Floyd.pdf |archivedate=2008-12-09 }})</ref><ref>C. A. R. Hoare. "[http://sunnyday.mit.edu/16.355/Hoare-CACM-69.pdf An axiomatic basis for computer programming] {{Wayback|url=http://sunnyday.mit.edu/16.355/Hoare-CACM-69.pdf |date=20110717175812 }}". ''Communications of the ACM'', 12(10):576–585, October 1969. {{doi|10.1145/363235.363259}}</ref>[[While循环]]的{{le|部分正确性|Partial correctness}}會由下列的规则所确定:

:<math>\frac{\{C\land I\}\;\mathrm{body}\;\{I\}} {\{I\}\;\mathbf{while}\ (C)\ \mathrm{body}\;\{\lnot C\land I\}}</math>

意思是：
* while 循环不可以使得 <math>I</math> 为假 - 如果在给定条件 <math>C</math> 下循环体 body 不會使不变量 <math>I</math> 从真变成假，则 <math>I</math> 在循环之前一样为真，在循环之后也會為真。
* 只要 <math>C</math> 為真時 <math>while(C)...</math> 必會循環。若其於循環之後中止，則 <math>C</math> 當為假。

==参见==
*[[循环不变代码外提]]
*[[不变条件]]
*{{le|循环变量|Loop variant}}

==参考文献==
{{reflist}}

[[Category:控制流程]]
[[Category:形式方法]]