在計算機科學中，循環不變數是程式循環的一個屬性，在每次疊代之前（和之後）都是真的。 這是一個邏輯斷言，有時通過斷言調用在代碼中檢查。 了解其不變數對於理解循環的影響至關重要。
在正式程式驗證中，特別是Floyd-Hoare方法，循環不變數由形式謂詞邏輯表示，並用於證明循環的屬性和通過使用循環的擴展算法（通常是正確性屬性）。 循環不變數在進入循環並且在每次疊代之後都是真的，因此在從循環退出時，可以保證循環不變數和循環終止條件。
基本介紹
- 中文名：循環不變代碼外提
- 領域：計算機科學
非正式的例子,程式語言支持,Eiffel,Whiley,使用循環不變數,
非正式的例子
下面的C子例程max（）返回其參數數組a []中的最大值，前提是它的長度n至少為1.注釋在第3,6,9,11和13行提供。每個注釋都有一個關於它的斷言 函式該階段的一個或多個變數的值。 循環體內，循環開始和結束時（第6行和第11行）的突出顯示的斷言完全相同。 因此，它們描述了循環的不變屬性。 當到達第13行時，該不變數仍然成立，並且已知來自第5行的循環條件i！= n變為假。 兩個屬性一起暗示m等於[0 ... n-1]中的最大值，即，從第14行返回正確的值。
int max(int n,const int a[]) {
int m = a[0];
// m equals the maximum value in a[0...0]
int i = 1;
while (i != n) {
// m equals the maximum value in a[0...i-1]
if (m < a[i])
m = a[i];
// m equals the maximum value in a[0...i]
++i; // m equals the maximum value in a[0...i-1] }
// m equals the maximum value in a[0...i-1]
, and i==n
return m;}
在防禦性編程範例之後，第5行中的循環條件i！= n應該更好地修改為i <n，以避免對n的非法負值進行無限循環。 雖然代碼中的這種變化直觀地應該沒有區別，導致其正確性的推理變得有點複雜，因為那時只有i> = n在第13行中已知。為了獲得它，i <= n成立， 條件必須包含在循環不變數中。 很容易看出i <= n也是循環的不變數，因為第6行中的i <n可以從第5行中的（修改的）循環條件獲得，因此i <= n保持在行中 在第10行中增加了i之後的情況。但是，當必須手動提供循環不變數以進行正式程式驗證時，諸如i <= n之類的直觀明顯的屬性經常被忽略。
程式語言支持
Eiffel
Eiffel程式語言為循環不變數提供原生支持。[4] 循環不變數用與類不變數相同的語法表示。 在下面的示例中，循環不變表達式x <= 10必須在循環初始化之後為真，並且在每次執行循環體之後; 這在運行時檢查。
from x := 0 invariant x <= 10 until x > 10 loop x := x + 1 end
Whiley
Whiley程式語言還為循環不變數提供了一流的支持。循環不變數使用一個或多個where子句表示，如下所示：
function max(int[] items) -> (int r)// Requires at least one element to compute maxrequires |items| > 0// (1) Result is not smaller than any elementensures all { i in 0..|items| | items[i] <= r }// (2) Result matches at least one elementensures some { i in 0..|items| | items[i] == r }: // nat i = 1 int m = items[0] // while i < |items| // (1) No item seen so far is larger than m where all { k in 0..i | items[k] <= m } // (2) One or more items seen so far matches m where some { k in 0..i | items[k] == m }: if items[i] > m: m = items[i] i = i + 1 // return m
max（）函式確定整數數組中的最大元素。要定義它，數組必須至少包含一個元素。 max（）的後置條件要求返回的值為：（1）不小於任何元素;並且，（2）它匹配至少一個元素。循環不變數通過兩個where子句歸納地定義，每個子句對應於後置條件中的子句。根本區別在於循環不變數的每個子句將結果標識為正確到當前元素i，而後置條件將結果標識為對所有元素都是正確的。
使用循環不變數
循環不變數可以用於以下目的之一：
純粹的紀錄片
通過斷言調用在代碼中進行檢查。
根據Floyd-Hoare方法進行驗證。
對於1.，自然語言注釋（如// m等於上例中[0 ... i-1]中的最大值）就足夠了。
對於2.，需要程式語言支持，例如C庫assert.h，或上面顯示的Eiffel中的不變子句。通常，運行時檢查可以通過編譯器或運行時選項打開（用於調試運行）和關閉（用於生產運行）。
對於3.，存在一些工具來支持數學證明，通常基於上面給出的Floyd-Hoare規則，給定的循環代碼實際上滿足給定的（一組）循環不變數。
抽象解釋技術可用於自動檢測給定代碼的循環不變數。但是，這種方法僅限於非常簡單的不變數（例如0 <= i && i <= n && i%2 == 0）。
