循环不变性是在算法中循环的前后都保持不变的一种属性。
利用循环不变性证明算法正确应该满足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