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

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

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

霍爾邏輯

編輯

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

 

意思是:

  • while 迴圈不可以使得   為假 - 如果在給定條件   下迴圈體 body 不會使不變數   從真變成假,則   在迴圈之前一樣為真,在迴圈之後也會為真。
  • 只要   為真時   必會循環。若其於循環之後中止,則   當為假。

參見

編輯

參考文獻

編輯
  1. ^ R. W. Floyd. "Assigning meanings to programs." Proceedings of the American Mathematical Society Symposia on Applied Mathematics. Vol. 19, pp. 19–31. 1967. (存档副本 (PDF). 2008-12-09 [2009-11-10]. (原始內容 (PDF)存檔於2008-12-09). )
  2. ^ C. A. R. Hoare. "An axiomatic basis for computer programming頁面存檔備份,存於網際網路檔案館)". Communications of the ACM, 12(10):576–585, October 1969. doi:10.1145/363235.363259