如何正確的理解循環不變式?
在演算法導論和accelerated c++ 中，都涉及到了循環不變式的概念，
兩者的意思本質大致相同，所以我的簡單的理解就是:
在循環中加入條件，然後人為的讓條件為真，達到「不變」的目的。直到我不需要這個循環了，就讓這個條件為假，循環終止。
而且，accelerated c++ 也提到了「不變式」，那麼，在while語句中，是否可以把條件式當做不變式？而「循環不變式」就是整個while語句體？還有，循環不變式和一般的循環，區別是否就在於條件式？新手，謝謝~~
佔位置明天來答
我才不告訴你我就是研究invariant generation的呢先回答你的問題。
首先不存在所謂的循環不變式和一般的循環的區別。其次不可以把條件式當作不變式。因為條件式在跳出while後不成立。下面是科普時間。
我們要建立一家生產火柴的小廠。
為了發展的好，我們要對火柴的質量有所保證（暫不考慮選址原料銷售等問題）。那我們該怎麼保證火柴的質量？員工小明說，每個火柴我們都點一下試試吧，這樣最保險。可保險是保險了，就算不考慮火柴還能不能用的問題，這其中的人力物力成本是無法承受的。這就是「窮舉」。員工小芳說，那我們就抽樣，每一百箱抽出一箱來做點燃實驗。如果抽樣的方法沒問題，這能體現火柴的質量。就是日常用的「黑盒測試」，搞一些測試用例來來看一下輸出是否滿足要求。員工小剛說，我們生產火柴的生產線有這麼多道工序，保證每道工序沒問題（上一工序輸出的產品符合要求，那麼經過這一工序，輸出的產品也沒問題）那麼最終的產品也沒有問題。這也是我們自查程序常用的方式。通常對於順序程序來說，每一語句都沒問題，那麼程序就沒問題。組長小菊說，小剛的方法不錯，可是我們引進的生產線里有環，怎麼辦呢？每次進入環的產品都不一樣啊。班長說，雖然有環，產品有區別，但他們都滿足一些性質，我們可以利用這些性質來確定最終產品合格。這個就是invariant。對於程序，驗證起來和上述過程差不多。而程序中控制語句大致有三種，一是通常的順序往下一步步執行，二是ifelse這種判斷，三是循環。對於前兩種，只要一步步的走就行了；而對於循環，我們需要找出不變數。（準確來說不變數是一種性質，且這個性質在多次循環中保持）這就是所謂的Hoare Logic。具體形式化的描述，參見維基百科。還是拿斐波那契數列舉例子，我們通常這麼寫：
//c++11
#include &
#include &
int fib1(int n) {
int a = 0, b = 1, tmp;
for(int i = 0; i &< n; ++i) {
tmp = a;
a = b;
b = b + tmp;
}
return a;
}
int main(){
printf("%d
", fib1(10));
return 0;
}
可以注意到，在fib1中，我們必須小心處理a，b，tmp三者的賦值順序，以確保下一個狀態的準確。 除此以外，i也是迭代過程中需要處理的狀態，這裡只是通過for循環來做了。
那麼如果這時候我要用《演算法導論》上提到的分析「循環不變式」的方法，來分析一下我寫的fib1正不正確，該怎麼做呢？
我們來理清一下，在a，b，tmp，i，n這5個變數中，tmp僅僅是用來解決賦值時的順序問題的，n是常量，真正跟迭代的狀態有關的變數是a，b，i這三個。
所以我們得到循環不變式：a == fib(i) b == fib(i + 1) ，只要我們能證明這個特質在從當前狀態到下一個狀態的過程中能得以保持（以及對初始狀態成立），我們就相當於證明了式子在迭代的每個階段都成立（有沒有發現其實就是數學歸納法？），我們就能確信我們的代碼沒有錯，即當i == n的時候，我們一定能得到a == fib(n)。
為了讓這件事情做得更機械一點，我們把代碼改寫成下面的fib2這樣，把迭代變數a，b，i都暴露出來，並且都通過next_*這些臨時變數來計算下一個狀態，這樣我們就只需要考慮下一個狀態和上一個狀態的關係，而不用關心賦值的順序了（可以注意到對next_*賦值的三條語句的順序是不重要的，對後面三條語句也一樣）。int fib2(int n) {
int a = 0, b = 1, i = 0, next_a, next_b, next_i; //(a, b, i) 構成一個狀態
while(true) {
if(i &>= n) {
break;
}
else {
next_a = b; //根據當前狀態計算下一個狀態
next_b = a + b;
next_i = i + 1;
a = next_a; //更新當前狀態
b = next_b;
i = next_i;
}
}
return a;
}
通過上面的改造，我們發現，在新的fib2中，迭代變數a，b，i已經被明確地暴露出來了，並且對下一個狀態的計算過程很明確，不再是搗鼓一些不明所以的tmp變數了，而且對計算順序也不再敏感。
不過，它顯然沒有fib1簡潔好看。那麼怎麼做到內外兼修呢？ 可以把迭代變數作為一組參數定義一個函數專門用來迭代，然後這組參數表達的就是當前狀態，在函數體內要做的主要事情，就是1. 判斷是否到達終止狀態， 2. 計算出下一個狀態。 這樣一來我們就得到了下面的fib3 。 可以看到，我們之前通過next_*變數做的事情，現在被傳參過程中的參數拷貝替代了。
int fib3(int n) {
std::function&
iter = [n, iter](int a, int b, int i) {
if(i &>= n) {
return a;
}
else {
return iter(b, b + a, i + 1);
}
};
return iter(0, 1, 0);
}
這樣做好處當然明顯，就是迭代變數一覽無餘，分析程序正確性更容易了。另外，計算下一個狀態的過程中也不需要考慮賦值的順序了，讀寫都方便很多。
但是這樣寫也是會帶來一些問題的，比如遞歸調用需要消耗棧內存空間，這樣一來程序就不可能長時間運行（因為每次迭代都要消耗內存空間）。
不過可以看到，以上的fib3和fib2是直接對應的，對於給出其中任何一種，我們都很容易機械地把它翻譯為另外一種，這種遞歸形式被稱為尾遞歸（見什麼是尾遞歸？ - 編程）。 既然人可以容易的在兩種形式之間轉換，那麼機器自然也能，所以在c++里，如果編譯的時候加了-O2的優化選項，這種形式的遞歸是可以僅佔用常量內存空間的。
所以從表達能力的角度考慮，那麼當然是應該把這種沒有副作用的純函數寫成遞歸的形式的。不過從實際使用的角度看，有相當多的非函數式語言（如Python，JavaScript）是不做尾遞歸優化的，所以在使用的時候也就要考慮這樣寫導致的佔用棧空間的代價，當然在非性能瓶頸處主要考慮的還是表達能力。循環不變式類似於程序的公理語義，主要用來做證明。
感覺類似歸納法吧，只不過不是無限的，多了一步終止來看看最後發生了什麼，是否正確
圖靈社區 : 圖書 : 循環不變式
就是一種證明程序正確性的形式化寫法，沒什麼特別的含義。
請看programming pearls第四章writing correct programs
推薦閱讀：