迴圈不變性是在演算法中迴圈的前後都保持不變的一種屬性。

利用迴圈不變性證明演算法正確應該滿足3個條件：（演算法導論中提到的）

初始條件: 首次迴圈前不變性成立
保持條件: 一次迴圈前不變性如果成立，則下次迴圈開始前不變性成立
終止條件: 迴圈結束後，迴圈不變性應能表明程式的正確性

例1（正確的程式）

def INSERTION_SORT(A):
    j = 1
    while j < len(A):
        key = A[j]
        i = j - 1
        while i >= 0 and key < A[i]:
            A[i+1] = A[i]
            i = i -1
        A[i+1] = key
        j = j + 1
 

要證明:  非降值插入排序演算法正確

迴圈不變性：A[0]到A[j-1]是非降值排序的

初始條件: j = 1 A[0] 為非降值排序的 成立
保持條件: 已知A[0]到A[j-1]是非降值排序的，第j次迴圈，會把A[j]排到適當的位置使執行完j=j+1語句後A[0]到A[j-1]仍然是非降值排序的
終止條件: 迴圈結束後，j = len(A), 則A[0]到A[len(A)-1]都是非降值排序的,這就表明了非降值插入排序演算法正確

例2（初始條件錯誤的程式）

def INSERTION_SORT(A):
    j = 2
    while j < len(A):
        key = A[j]
        i = j - 1
        while i >= 0 and key < A[i]:
            A[i+1] = A[i]
            i = i -1
        A[i+1] = key
        j = j + 1
 

要證明:  非降值插入排序演算法正確

迴圈不變性：A[0]到A[j-1]是非降值排序的

初始條件: j = 2 A[0] 到A[1]不一定為非降序排列的， 演算法不正確

例3（終止條件錯誤的程式）

def INSERTION_SORT(A):
    j = 1
    while j < len(A) - 1:
        key = A[j]
        i = j - 1
        while i >= 0 and key < A[i]:
            A[i+1] = A[i]
            i = i -1
        A[i+1] = key
        j = j + 1
 

要證明:  非降值插入排序演算法正確

迴圈不變性：A[0]到A[j-1]是非降值排序的

初始條件: j = 1 A[0] 為非降值排序的， 成立
保持條件: 已知A[0]到A[j-1]是非降值排序的，第j次迴圈，會把A[j]排到適當的位置使執行完j=j+1語句後A[0]到A[j-1]仍然是非降值排序的

終止條件: 迴圈結束後，j = len(A) -1 , 則A[0]到A[len(A)-2]都是非降值排序的,但不能證明A[0]到A[len(A)-1]都是非降值排序的，演算法不正確

既然是不變的特性，如果方便的話，就可以用程式來判斷其正確性了，加入斷言可以達到這個效果，下面這個例子未必恰當，只是展示如何用斷言判斷不變性：

#!python
#Insertion sort
def is_sorted(A, j):
    if j == 0:
        return True
    for i in range(1, j):
        if A[i] < A[i-1]:
            print "error: A[%d] < A[%d]" % (i, i-1)  
            return False
    return True
def INSERTION_SORT(A):
    j = 1
    assert is_sorted(A, j)
    while j < len(A):
        assert is_sorted(A, j)
        key = A[j]
        i = j - 1
        while i >= 0 and key < A[i]:
            A[i+1] = A[i]
            i = i -1
        A[i+1] = key
        j = j + 1
        assert is_sorted(A, j)
    assert j== len(A)
a = [5, 2, 4, 6, 1, 3]
if __name__ == "__main__":
    print "the length of list a is:", len(a)
    print "list a have:", a
    INSERTION_SORT(a)
    print "After insert-sort, a is:", a