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

我将为你详细讲解如何用循环不变式证明快速排序的正确性。这是一个深入理解算法正确性的重要方法。

题目描述
使用循环不变式（Loop Invariant）来严格证明快速排序算法的正确性。循环不变式是一种在算法执行过程中始终保持为真的性质，用于证明算法的正确性。

解题过程

1. 快速排序算法回顾
首先我们回顾快速排序的基本步骤：

def quicksort(A, p, r):
    if p < r:
        q = partition(A, p, r)  # 划分数组
        quicksort(A, p, q-1)    # 递归排序左半部分
        quicksort(A, q+1, r)    # 递归排序右半部分

def partition(A, p, r):
    x = A[r]  # 主元（pivot）
    i = p - 1
    for j in range(p, r):
        if A[j] <= x:
            i += 1
            A[i], A[j] = A[j], A[i]
    A[i+1], A[r] = A[r], A[i+1]
    return i + 1

2. 理解循环不变式的概念
循环不变式是在循环的每次开始和结束时都为真的性质。我们需要为partition函数中的循环找到一个合适的不变式。

3. 定义partition函数的循环不变式
对于partition函数中的循环，我们定义以下循环不变式：
在循环的每次迭代开始时，对于任意索引k：

• 如果 p ≤ k ≤ i，那么 A[k] ≤ x（主元）
• 如果 i+1 ≤ k ≤ j-1，那么 A[k] > x
• 如果 k = r，那么 A[k] = x

4. 证明循环不变式的三个性质

初始化（Initialization）
在循环开始前（j = p）：

• i = p-1，所以第一个区间 p ≤ k ≤ i 为空（因为i < p）
• j-1 = p-1，所以第二个区间 i+1 ≤ k ≤ j-1 也为空
• 第三个条件显然成立
  因此，初始化时循环不变式成立。

保持（Maintenance）
假设在第j次迭代开始时循环不变式成立，考虑两种情况：

情况1：A[j] ≤ x

• i增加1，交换A[i]和A[j]
• 交换后A[i] ≤ x（满足第一个条件）
• 原来的A[i+1]（现在是A[j]）> x（满足第二个条件）

情况2：A[j] > x

• i不变，j增加1
• A[j]自动进入第二个区间（满足第二个条件）

在两种情况下，循环不变式都得到保持。

终止（Termination）
当循环结束时，j = r：

• 所有元素A[p...i] ≤ x
• 所有元素A[i+1...r-1] > x
• A[r] = x

最后交换A[i+1]和A[r]，得到：

• A[p...i] ≤ x
• A[i+1] = x
• A[i+2...r] > x

5. 证明快速排序的整体正确性

基本情况
当p ≥ r时，数组已经有序（空数组或单元素数组），算法正确。

归纳步骤
假设对于所有大小小于n的数组，快速排序都能正确排序。对于大小为n的数组：

1. partition函数将数组划分为三部分
2. 左半部分和右半部分的大小都小于n
3. 根据归纳假设，递归调用能正确排序这两个子数组
4. 由于左半部分所有元素 ≤ 主元 ≤ 右半部分所有元素，整个数组有序

6. 边界条件处理
循环不变式还能帮助我们验证边界条件的正确性：

• 当数组为空时，p > r，直接返回
• 当所有元素都相等时，partition仍能正确工作
• 当数组已排序时，算法仍能正确终止

7. 总结
通过循环不变式，我们严格证明了：

1. partition函数能正确划分数组
2. 快速排序的递归结构能保证最终结果有序
3. 所有边界情况都能得到正确处理

这种证明方法不仅适用于快速排序，也可以推广到其他分治算法，是算法正确性分析的重要工具。