正确的算法

对任意一个输入，算法能得到一个正确的输出

循环不变量

与程序变量有关的一个语句，他在循环刚开始前，以及在循环的每个迭代执行后为真，特别是在循环结束后，任然为真

插入排序算法伪代码

# A是需要被排序的无序序列，假设A中的元素从1开始计数
InsertSort(A)
    for j = 2 to n do
        key = A[j]    // 将当前需要被插入到已经排好序的序列的元素A[j]存到中间变量key中
        i = j-1
        while i > 0 and A[i] > key do    // 在已经排好序的序列中去找到A[j]的插入位置
            A[i+1] = A[i]    // 往后移动一位
            i = i-1
        A[i + 1] = key    // 将A[j]插入到合适的位置
return A

插入排序的循环不变量

在for循环第j个迭代执行前，子数组A[1,…,j-1]由最初A[1,…,j-1]中的元素构成，不过现在 是有序的

算法的正确性

• 数学归纳法：
  1. 当n=0的时候，怎么样
  2. 假设：当n=k的时候，怎么样
  3. 验证：当n=k+1的时候，怎么样
  4. 所以：当n=的时候怎么样
• 利用循环不变量证明算法的正确性

寻找到循环不变量，即某个特性,然后证明循环不变量为真(j=1,…,n),然后利用类似数学归纳法的证明方法：

1. 初始布：在循环的迭代开始前，为真；
2. 归纳步：如果在循环的第j个迭代前，为真，则在循环的第j+1个迭代前，为真；
3. 终止步：当循环终止时，为真。

   插入排序算法的正确性证明

• 插入排序的循环不变量：当j=k的时候，序列A[k-1]个元素还是没有排序前的那k-1个元素，但是现在的k-1个元素是已经排好序的k-1个元素
• 循环不变量;j=k
• :A[1],…,A[k-1],是有序的，且还是原来没有排序的那些元素
• 证明：
  1. 初始补：j = 2
     1. 
  2. 当j = k的时候：
     1. 假设是有序的 // 也就是假设循环不变量是正确的
  3. 验证，当j = k+1的时候，去验证循环不变量的正确性：
     1. = ？
     2. 去对运行算法，验证的正确性，也就是验证是不是有序的序列