排序算法之：循环不变式在插入排序中的正确性证明

题目描述：使用循环不变式（Loop Invariant）来证明插入排序算法的正确性。插入排序的基本思想是将数组分为已排序和未排序两部分，每次从未排序部分取出一个元素，插入到已排序部分的正确位置。

解题过程：

1. 理解循环不变式的概念
   循环不变式是在循环的每次迭代开始和结束时都为真的条件。它帮助证明算法的正确性，需要满足三个性质：

• 初始化：在循环第一次迭代开始前为真
• 保持：如果某次迭代开始前为真，那么下次迭代开始前也保持为真
• 终止：循环终止时，不变式能证明算法的正确性

2. 插入排序算法描述

def insertion_sort(arr):
    n = len(arr)
    # 循环不变式：arr[0...i-1]是已排序的
    for i in range(1, n):  # i从1到n-1
        key = arr[i]  # 当前要插入的元素
        j = i - 1
        # 将arr[i]插入到arr[0...i-1]的正确位置
        while j >= 0 and arr[j] > key:
            arr[j + 1] = arr[j]  # 向右移动元素
            j -= 1
        arr[j + 1] = key  # 插入到正确位置

3. 定义循环不变式
   对于外层循环（i从1到n-1），定义循环不变式：
   "子数组arr[0...i-1]包含原数组中前i个元素，且这些元素已按升序排列"

4. 证明初始化性质

• 在第一次迭代开始前（i=1），子数组arr[0...0]只包含第一个元素
• 单个元素的数组自然是有序的
• 因此循环不变式在初始化时成立

5. 证明保持性质

• 假设在第i次迭代开始前，arr[0...i-1]已排序
• 内层循环的工作：
  • 从j=i-1开始向左扫描
  • 将所有大于key的元素向右移动一位
  • 找到第一个≤key的元素位置
  • 将key插入到该位置后面
• 执行后，arr[0...i]包含原数组前i+1个元素且保持有序
• 因此循环不变式在下次迭代开始前仍然成立

6. 证明终止性质

• 当i=n时循环终止
• 此时循环不变式表明：arr[0...n-1]包含所有n个元素且已排序
• 这正是排序算法要达到的目标

7. 时间复杂度分析

• 最坏情况：数组完全逆序，每次插入需要比较i次
• 总比较次数：1 + 2 + ... + (n-1) = n(n-1)/2 = O(n²)
• 最好情况：数组已排序，每次插入只需比较1次 = O(n)
• 平均情况：O(n²)

8. 空间复杂度分析

• 只需要常数级别的额外空间（key, i, j等变量）
• 空间复杂度为O(1)，是原地排序算法

通过循环不变式的严格证明，我们可以确信插入排序算法确实能正确地将数组排序。这种方法不仅适用于插入排序，也可以用于证明其他排序算法的正确性。