迴圈不變數

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

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

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

霍爾邏輯

在弗洛伊德-霍爾邏輯，^[1][2]While迴圈的部分正確性（英語：Partial correctness）會由下列的規則所確定:

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

意思是：

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

參見

• 迴圈不變代碼外提
• 不變條件
• 迴圈變數（英語：Loop variant）