循環不變式 - 菜鳥學院

引言

　　算法程序形式化設計和證明是確保算法程序邏輯結構正確的最理想途徑，是保證軟件可靠性的有效手段之一；而體現了算法程序本質特徵的循環不變式在算法程序形式化方法中具有十分重要的作用。循環不變式是程序設計理論中的一個重要概念。這一概念的建立在程序設計從藝術走向科學這一歷史性的轉變過程中起着巨大的推動作用，它不僅可以幫助人們理解那些難以理解的、精巧的循環算法程序，而且可以用來形式化地證明循環算法程序的正確性，也有助於形式化地開發出高質量的循環程序。

　　然而循環不變式的開發一直是算法程序設計領域中最具挑戰性、最富有創造性的問題之一，許多計算機科學家和計箅機工作者也致力於這方面的研究。目前，人們把循環不變式定義爲在循環的每次執行前後都爲真的謂詞。

本文地址：http://www.cnblogs.com/archimedes/p/loop-invariant.html，轉載請註明源地址。

定義

循環不變式：反映循環體中所有循環變量的變化規律並在循環體執行前後都爲真的謂詞稱爲該循環體的循環不變式。

循環變量：在循環體中，其值隨着循環體的執行不斷髮生變化的變量稱爲循環變量。

算法導論第二章中的原文是：We state these properties of A[1 ‥ j -1] formally as a loop invariant。其中舉的例子是插入排序，每次循環從數組A中取出第j個元素插入有序區A[1 .. j-1]，然後遞增j。這樣A[1 .. j-1]的有序性始終得到保持，這就是所謂的「循環不變 (loop invariant)」了。

這個概念主要用來檢驗算法的正確性。原文如下：

We use loop invariants to help us understand why an algorithm is correct. We must show three things about a loop invariant:

Initialization: It is true prior to the first iteration of the loop.

Maintenance: If it is true before an iteration of the loop, it remains true before the next iteration.

Termination: When the loop terminates, the invariant gives us a useful property that helps show that the algorithm is correct.

1. 初始化（循環第一次迭代之前）的時候，A[1 ‥ j -1]的「有序性」是成立的；

2. 在循環的每次迭代過程中，A[1 ‥ j -1]的「有序性」仍然保持；

3. 循環結束的時候，A[1 ‥ j -1]的「有序性」仍然成立。

編寫循環時，找到讓每次循環都成立的邏輯表達式很重要。這種邏輯表達式稱爲循環不變式（loop invariant）。循環不變式相當於用數學歸納法證明的「斷言」。

循環不變式用於證明程序的正確性。在編寫循環時，思考一下「這個循環的循環不變式是什麼」就能減少錯誤。

舉例應用

以一個非常簡單的例子來講解循環不變式吧。

代碼清單是用C 語言寫的sum 函數，功能是求出數組元素之和。參數array[] 是要求和的對象數組，size 是這個數組的元素數。調用sum 函數，會獲得array[0] 至array[size-1] 的size 個元素之和。

代碼清單--sum函數，求出數組的元素之和

int sum(int array[], int size)
{
    int k = 0;
    int s = 0;
    while(k < size) {
        s = s + array[k];
        k = k + 1;
    }
    return s;
}

在sum 函數中使用了簡單的while 循環語句。我們從數學歸納法的角度來看這個循環，得出下述斷言M(n)。這個斷言就是循環不變式。

• 斷言M (n ) ：數組array 的前n 個元素之和，等於變量s 的值。

我們在程序中成立的斷言上標註註釋，形成清單4-3 所示代碼。

代碼清單--在上面的代碼中成立的斷言上標註註釋

在代碼清單的第4 行，s 初始化爲0。由此，第5 行的M(0) 成立。M(0) 即爲「數組array 的前0 個元素之和等於變量s 的值」。這相當於數學歸納法的步驟1。

數學歸納法的步驟1（M(0)成立）

第7 行中，M(k) 成立。然後進行第8 行的處理，將數組array[k] 的值加入s, 因此M(k+1) 成立。這相當於數學歸納法的步驟2。

數學歸納法的步驟2（M(k) M(k+1)成立）

請一定要理解第8 行，
s=s+array[k];

意爲「在M(k) 成立的前提下，M(k+1) 成立」。

第10 行中k 遞增1，所以第11 行的M(k) 成立。這裏是爲了下一步處理而設定變量k的值。

最後，第13 行的M(size) 成立。因爲while 語句中的k 遞增了1，而這時一直滿足M(k), 走到第13 行時k 和size 的值相等。M(size) 成立說明sum 函數是沒有問題的。因此，第14 行return 返回結果。

M (size )成立

綜上所述，這個循環在k 從0 增加到size 的過程中一直保持循環不變式M(k) 成立。編寫循環時，有兩個注意點。一個是「達到目的」，還有一個是「適時結束循環」。循環不變式M(k) 就是爲了確保「達到目的」。而k 從0 到size 遞增確保了「適時結束循環」。

在下面的代碼清單中，寫明瞭M(k) 成立的同時k 遞增的情形。（∧表示「並且」）

代碼清單-- M (k )成立的同時k遞增

參考資料：

《算法導論》

《循環不變式開發新策略及其應用》