迴圈不變式

迴圈不變式其主要是用來幫助我們理解和證明演算法的正確性。
關於迴圈不變式我們必須證明三個性質：

• 初始化：它在迴圈的第一輪迭代開始之前，應該是正確的。
• 保持：如果在某一次迴圈迭代開始之前是正確的，那麼在下一次迭代開始之前，它也應該保持正確。
• 結束：當迴圈結束時，不變式給了我們一個有用的性質，它有助於表明演算法是正確的。

插入排序的證明

for j = 2 to A.length
    key = A[j]
    // Insert A[j] into the sorted sequence A[1..j-1].
    i = j-1
    while i > 0 and A[i] > key
        A[i+1] = A[i]
        i = i -1
    A[i+1] = key
 

• 初始化：在第一輪迭代開始之前，證明其正確性。此時j=2，A[1…j-1]中只有一個元素A[1]，顯然，一個元素是已經排序的了。所以，證明了迴圈不變式在第一輪迭代之前是成立的。
• 保持：接下來要證明在每輪迭代中，迴圈不變式保持成立。迭代之前，假設A[1…j-1]是已經排好序的序列，待排序的元素A[j]依次與A[j-1]、A[j-2]進行比較，如果A[j-1]等大於A[j]，則依次將其向右移動一位，當遇到開始小於A[j]的元素時，則A[j]找到了合適的插入位置，插入之後，整個序列又是排好序的了。即在假設j成立的情況下，j+1也成立，迴圈不變式在迭代過程中保持成立。
• 終止：最後，分析一下迴圈結束時候的情況。當j=n+1時，迴圈結束，此時A[1…n]中已經有n個元素，且已經排好序，就是排好序的陣列A[1…n]，所以演算法正確。