初始化：它在迴圈的第一輪迭代開始之前，應該是正確的。
保持：如果在某一次迴圈迭代開始之前是正確的，那麼在下一次迭代開始之前，它也應該保持正確（假設當迴圈變數等於k時符合，再看執行一遍迴圈體後是否還符合迴圈不變式）。
結束：當迴圈結束時，不變式給了我們乙個有用的性質，它有助於表明演算法是正確的（這一步是和數學歸納法不同的一點，用迴圈不變式則更進一步，數學歸納法到這裡就得出了乙個關係式就結束，而用迴圈不變式，不但要先確保乙個正確的關係式，還要看最後迴圈結束時，迴圈變數最後等於多少，根據迴圈不變式推導是否符合自己的要求。）。
編寫迴圈時，讓每次迴圈都成立的邏輯表示式稱為迴圈不變式（loop invariant）。
注意：每個迴圈都可以找到乙個迴圈不變式，我們可以通過這個迴圈不變式證明迴圈迭代的正確性。
案例分析
利用迴圈不變數證明下述計算a^n演算法的正確性：
exp(a,n)
1 i<--1
2 pow<--1
3 while i<=n do
4 pow<-pow*a
5 i<--i+1
6 return pow
初始化：迴圈開始之前，i=1，pow=a^(i-1)=1，等式成立，所以迭代之前迴圈不變式成立。
保持：假設i=k的時候迴圈不變式成立,此時還未執行迴圈語句，迴圈不變式成立，即a^(k-2)=1，則在迴圈中執行的pow=pow*a,那麼pow=a^(k-1)。即在迭代過程中，迴圈不變式保持成立。
終止：當k=n+1時，迴圈終止，此時pow=a^n。所以演算法終止時，得到的是乙個正確的結果，返回了a的n次冪。
《演算法基礎 開啟演算法之門》一2 3 迴圈不變式
對於線性查詢的3個演算法，我們能很容易地看到每個演算法均能生成正確的結果。但是有時候生成正確的結果看起來有點難。這涉及一系列技術，在這裡不能一一講解。證明正確性的乙個常用方法是使用迴圈不變式證明 即證明迴圈的每次迭代之前迴圈不變式為真。迴圈不變式能夠幫助我們證明正確性，關於迴圈不變式，我們必須證明以...
演算法基礎 使用迴圈不變式解決插入排序問題
思想是直接插入排序，即每次拿乙個數字向已排序好的數字中插入，採用迴圈不變式的設計思想。迴圈不變式 一般而言,用這個式子表示希望得到的結果,如果在迴圈的每一步,這個式子都是正確的,那麼迴圈結束後,這個式子也正確,並得到了期望的結果。如何證明迴圈的每一步式子都是正確的？需要證明式子滿足三個性質 初始化 ...
迴圈不變式的思想及其應用
迴圈不變式的思想及其應用 迴圈不變式 loop invariants 不只是一種電腦科學的思想，準確地說是一種數學思想。在數學上闡述了通過迴圈 迭代 遞迴 去計算乙個累計的目標值的正確性，屬於基礎數學的範疇，而且在計算機上也應用廣泛。初次見到這個詞是在 演算法導論 在第二章描述了這個思想和正確性，後...