循環不變數

循環不變數（loop invariant）是一個不變數，被用來證明循環的特點，更多地，算法使用循環 (usually 正確性)。非正式的說，一個循環不變數是指在循環開始和循環中每一次疊代時永遠為真的量，這意味著在循環中和循環結束時循環不變數和循環終止條件必須同時成立。

基本介紹

• 中文名：循環不變數
• 外文名：loop invariant
• 性質：不變數
• 領域：計算機

概述

由於循環和遞歸的程式相似的原因，證明帶有不變數的循環的部分正確性和證明通過歸納的遞歸程式的正確性極其相似。事實上，循環不變數通常是一個遞歸程式可以等價為一個給定循環的遞歸的屬性。

霍爾邏輯

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

意思是：

一個 while 循環不可以使得 為假 - 如果在給定條件 下循環體 body 不會使不變數從真變成假，則 將在循環之後如在循環之前一樣為真。

只要 為真時必會循環。若其於循環之後中止，則當為假。

循環不變代碼外提

循環不變代碼外提（英語：loop-invariant code motion，縮寫LICM）在計算機編程中是指將循環不變的語句或表達式移到循環體之外，而不改變程式的語義。循環不變代碼外提在英文中又被稱為hoisting或scalar promotion，是編譯器中常見的最佳化方法。

循環不變數

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

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

遞歸

遞歸（英語：Recursion），又譯為遞迴，在數學與計算機科學中，是指在函式的定義中使用函式自身的方法。遞歸一詞還較常用於描述以自相似方法重複事物的過程。例如，當兩面鏡子相互之間近似平行時，鏡中嵌套的圖像是以無限遞歸的形式出現的。也可以理解為自我複製的過程。

歸經常被用於解決計算機科學的問題。在一些程式語言（如Scheme、Haskell中），遞歸是進行循環的一種方法。