迴圈不變數

在電腦科學中，迴圈不變式（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$ 當為假。

參見

• 迴圈不變代碼外提
• 不變條件
• 迴圈變數