循環不變量

在計算機科學中，循環不變式（loop invariant，或循環不變量、循環不變條件，也有譯作循環不變性），是一組在循環體內、每次迭代均保持為真的性質（表達式），通常被用來證明程式或偽碼的正確性（有時但較少情況下用以證明算法的正確性）。簡單說來，「循環不變式」是指在循環開始和循環中，每一次迭代時為真的性質。這意味着，一個正確的循環體，在循環結束時「循環不變式」和「循環終止條件」必須同時成立。

由於循環和遞歸的相通，證明帶有不變式的循環的部分正確性和證明通過歸納的遞歸程序的正確性極其相似。

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

霍爾邏輯

在弗洛伊德-霍爾邏輯，While循環的部分正確性會由下列的規則所確定:

${\frac {\{C\land I\}\;\mathrm {body} \;\{I\}}{\{I\}\;\mathbf {while} \ (C)\ \mathrm {body} \;\{\lnot C\land I\}}}$

意思是：

• while 循環不可以使得 $I$ 為假 - 如果在給定條件 $C$ 下循環體 body 不會使不變量 $I$ 從真變成假，則 $I$ 在循環之前一樣為真，在循環之後也會為真。
• 只要 $C$ 為真時 $while(C)...$ 必會循環。若其於循環之後中止，則 $C$ 當為假。

參見

• 循環不變代碼外提
• 不變條件
• 循環變量