循环不变式
引言
算法程序形式化設(shè)計和證明是確保算法程序邏輯結(jié)構(gòu)正確的最理想途徑，是保證軟件可靠性的有效手段之一；而體現(xiàn)了算法程序本質(zhì)特征的循環(huán)不變式在算法程序形式化方法中具有十分重要的作用。循環(huán)不變式是程序設(shè)計理論中的一個重要概念。這一概念的建立在程序設(shè)計從藝術(shù)走向科學(xué)這一歷 史性的轉(zhuǎn)變過程中起著巨大的推動作用，它不僅可以幫助人們理解那些難以理解的、精巧的循環(huán)算法程序，而且可以用來形式化地證明循環(huán)算法程序的正確性，也有助于形式化地開發(fā)出高質(zhì)量的循環(huán)程序 。
然而循環(huán)不變式的開發(fā)一直是算法程序設(shè)計領(lǐng)域中最具挑戰(zhàn)性、最富有創(chuàng)造性的問題之一，許多計算機科學(xué)家和計箅機工作者也致力于這方面的研究。目前，人們把循環(huán)不變式定義為在循環(huán)的每次執(zhí)行前后都為真的謂詞 。
本文地址：http://www.cnblogs.com/archimedes/p/loop-invariant.html，轉(zhuǎn)載請注明源地址。
定義
循環(huán)不變式：反映循環(huán)體中所有循環(huán)變量的變化規(guī)律并在循環(huán)體執(zhí)行前后都為真的謂詞稱為該循環(huán)體的循環(huán)不變式 。
循環(huán)變量：在循環(huán)體中，其值隨著循環(huán)體的執(zhí)行不斷發(fā)生變化的變量稱為循環(huán)變量 。
算法導(dǎo)論第二章中的原文是：We state these properties of A[1 ‥ j -1] formally as a loop invariant。其中舉的例子是插入排序，每次循環(huán)從數(shù)組A中取出第j個元素插入有序區(qū)A[1 .. j-1]，然后遞增j。這樣A[1 .. j-1]的有序性始終得到保持，這就是所謂的“循環(huán)不變 (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. 初始化（循環(huán)第一次迭代之前）的時候，A[1 ‥?j?-1]的“有序性”是成立的；
2. 在循環(huán)的每次迭代過程中，A[1 ‥?j?-1]的“有序性”仍然保持；
3. 循環(huán)結(jié)束的時候，A[1 ‥?j?-1]的“有序性”仍然成立。
編寫循環(huán)時，找到讓每次循環(huán)都成立的邏輯表達式很重要。這種邏輯表達式稱為循環(huán)不變式（loop invariant）。循環(huán)不變式相當(dāng)于用數(shù)學(xué)歸納法證明的“斷言”。
循環(huán)不變式用于證明程序的正確性。在編寫循環(huán)時，思考一下“這個循環(huán)的循環(huán)不變式是什么”就能減少錯誤。
舉例應(yīng)用
以一個非常簡單的例子來講解循環(huán)不變式吧。
代碼清單是用C 語言寫的sum 函數(shù)，功能是求出數(shù)組元素之和。參數(shù)array[] 是要求和的對象數(shù)組，size?是這個數(shù)組的元素數(shù)。調(diào)用sum 函數(shù)，會獲得array[0] 至array[size-1] 的size?個元素之和。
代碼清單--sum函數(shù)，求出數(shù)組的元素之和
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 函數(shù)中使用了簡單的while 循環(huán)語句。我們從數(shù)學(xué)歸納法的角度來看這個循環(huán)，得出下述斷言M(n)。這個斷言就是循環(huán)不變式。
? 斷言M (n ) ：數(shù)組array 的前n 個元素之和，等于變量s 的值。
我們在程序中成立的斷言上標(biāo)注注釋，形成清單4-3 所示代碼。
代碼清單--在上面的代碼中成立的斷言上標(biāo)注注釋
在代碼清單的第4 行，s 初始化為0。由此，第5 行的M(0) 成立。M(0) 即為“數(shù)組array 的前0 個元素之和等于變量s 的值”。這相當(dāng)于數(shù)學(xué)歸納法的步驟1。
數(shù)學(xué)歸納法的步驟1（M(0)成立）
第7 行中，M(k) 成立。然后進行第8 行的處理， 將數(shù)組array[k] 的值加入s, 因此M(k+1) 成立。這相當(dāng)于數(shù)學(xué)歸納法的步驟2。
數(shù)學(xué)歸納法的步驟2（M(k) M(k+1)成立）
請一定要理解第8 行，
s=s+array[k];
意為“在M(k) 成立的前提下，M(k+1) 成立”。
第10 行中k 遞增1，所以第11 行的M(k) 成立。這里是為了下一步處理而設(shè)定變量k的值。
最后，第13 行的M(size) 成立。因為while 語句中的k 遞增了1，而這時一直滿足M(k), 走到第13 行時k 和size 的值相等。M(size) 成立說明sum 函數(shù)是沒有問題的。因此，第14 行return 返回結(jié)果。
M (size )成立
綜上所述，這個循環(huán)在k 從0 增加到size 的過程中一直保持循環(huán)不變式M(k) 成立。編寫循環(huán)時，有兩個注意點。一個是“達到目的”，還有一個是“適時結(jié)束循環(huán)”。循環(huán)不變式M(k) 就是為了確保“ 達到目的”。而k 從0 到size 遞增確保了“適時結(jié)束循環(huán)”。
在下面的代碼清單中，寫明了M(k) 成立的同時k 遞增的情形。（∧表示“并且”）
代碼清單-- M (k )成立的同時k遞增
?參考資料：
《算法導(dǎo)論》
《循環(huán)不變式開發(fā)新策略及其應(yīng)用》
圖靈社區(qū)--循環(huán)不變式
?
總結(jié)
- 上一篇： 在线富文本编辑器FckEditor配置（
- 下一篇： 竞态条件与临界区