如何证明算法的正确性？

结合算法导论相关章节的学习，利用号循环不变式可以帮助我们理解算法的正确性。循环不等式主要满足以下的三条性质：

初始化：循环的第一次迭代之前，它为真。

保持：如果循环的某次迭代之前它为真，那么下次迭代之前它仍为真

终止：在循环终止之前，不变式为我们提供一个有用的性质，该性质有助于证明算法是正确的。

插入排序算法正确性

INSERTION-SORT(A)
for j = 2 to A.length
key = A[j]
i = j - 1
while i > 0 and A[i] > key
A[i+1] = A[i]
i = i - 1
A[i+1] = A[j]

接着使用循环不变式来证明正确性：

初始化：先证明在第一次循环迭代之前，循环不等式成立（j = 2）。所以子数组A[1…j-1]仅有单个元素A[1]组成，实际上就是A[1]中原来的元素。该元素只有一个且已经排好序。这表明第一次循环迭代之前循环不变式成立。

保持：接着处理第二条性质：证明每次迭代保持循环不等式。非形式化地，for循环体中的第4-7行将A[j-1]、A[j-2]、A[j-3]等向后移动一个位置，直到找到A[j]的适当位置，第8行将A[j]的值插入到该位置。此时，整个子数组A[1…j]由原来的A[1…j]中的元素组成，但已按序排列，那么对于for循环的下一次迭代将怎加j保持循环不变式。

终止：最后研究在循环终止时发生了什么。导致for循环终止的条件是j>A.length=n。因此为每次循环迭代j增加1，那么必有j = n+1。在循环不变式的表述中将j用n+1代替，我们有：子数组A[1…n]由原来在A[1…n]中的元素组成，但都已经按序排列。A[1…n]已经是整个数组故算法正确。

归并排序算法正确性

MERGE(A,p,q,r)
n1 = q - p + 1
n2 = r - q
for i = 1 to n1
L[i] = A[p + i - 1]
for j = 1 to n2
R[j] = A[q + j]
L[n1 + 1] = 无穷
R[n2 + 1] = 无穷
i = 1
j = 1
for k = p to r
if L[i] <= R[j]
A[k] = L[i]
i = i + 1
else A[k] = R[j]
j = j + 1

我们必须证明第12-17行for循环的第一次迭代之前该循环不变式成立，该循环的每次迭代保持该不变式，并且循环终止时，该不变式提供一种有用的性质来证明正确性。

初始化：循环的一次迭代之前，有k=p，所以子数组A[p…k-1]为空。这个空的子数组包含L和R的k-p=0个最小元素。又因为i=j=1，所以L[i]和R[j]都是各自所在数组中未被赋值回数组A的最小元素。

保持：为方便理解，假设L[i] <= R[j]。这时，L[i]是未被复制回数组A的最小元素。因为A[p..k-1]包含k-p个最小元素，所以在第14行将L[i]复制到A[k]之后，子数组A[p..k]将包含k-p+1个最小元素，增加k的值和i的值，为下次迭代重新建立该循环不等式，反之，若L[i] > R[j]，则根据16-17行执行适当的操作来维持该循环不等式。

终止：终止时k = r+1。根据循环不等式，子数组A[p..k-1]就是A[p..r]且按从小到大的顺序包含L[1..n1+1]和R[1..n2+1]中的k-p=r-p+1个最小元素。数组L和R一起包含n1 + n2 + 2 = r - p + 3个元素。除两个最大元素以外，其它所有元素都已经被复制回数组A。