循环不变性（loop invariant）-证明算法的正确性的一种方法

循环不变性是在算法中循环的前后都保持不变的一种属性。

利用循环不变性证明算法正确应该满足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