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

题目描述：
归并排序采用分治策略，将数组递归地分成两半，分别排序后合并。我们需要使用循环不变式来严格证明归并排序中合并步骤的正确性。具体来说，假设有两个已排序的数组左半部分 L[0..p-1] 和右半部分 R[0..q-1]，合并过程需将二者按序合并到原数组 A[k..r] 中。要求通过循环不变式证明合并后 A[k..r] 是有序的。

解题步骤

1. 理解合并过程的关键逻辑

合并步骤的伪代码如下：

合并(L, R, A, k, r):
    i = 0, j = 0, index = k   // i遍历L，j遍历R，index写入A
    while i < p and j < q:
        if L[i] ≤ R[j]:
            A[index] = L[i]
            i += 1
        else:
            A[index] = R[j]
            j += 1
        index += 1
    // 将剩余元素复制到A
    while i < p:
        A[index] = L[i]
        i += 1, index += 1
    while j < q:
        A[index] = R[j]
        j += 1, index += 1

2. 定义循环不变式

在合并的主循环（第一个 while）中，定义循环不变式为：
每次循环迭代开始时，子数组 A[k..index-1] 已按非递减顺序包含 L[0..i-1] 和 R[0..j-1] 中的所有元素，且 A[index-1] ≤ min(L[i], R[j])（若 L 或 R 有剩余）。

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

• 初始化：
  循环开始时，i=0, j=0, index=k。此时 A[k..index-1] 为空，包含 L[0..-1] 和 R[0..-1]（空集），有序条件自然满足。由于 L 和 R 非空时 min(L[i], R[j]) 存在，条件成立。

• 保持：
  假设某次迭代前不变式成立。本次迭代会比较 L[i] 和 R[j]，将较小值（设为 x）放入 A[index]。由于此前 A[index-1] ≤ x（由不变式中的最小值条件保证），且 x 来自当前未处理部分的最小值，因此 A[k..index] 仍有序。更新 i 或 j 后，新的 L[i] 和 R[j] 均不小于 x，故 A[index] ≤ min(L[i], R[j]) 继续成立。

• 终止：
  循环结束时，i=p 或 j=q。假设 i=p（左半部分耗尽），则剩余元素均来自 R[j..q-1]。由不变式，A[k..index-1] 已有序且 A[index-1] ≤ R[j]，而 R 本身有序，因此直接复制剩余部分可保持整体有序。另一情况对称。

4. 扩展到递归过程的正确性

• 基础情况：当子数组长度为 1 时，天然有序。
• 归纳步骤：假设归并排序能正确排序左右半部分，再通过上述合并步骤的正确性，可证明整个数组有序。

总结

通过循环不变式严格验证了合并操作的可靠性，结合分治法的归纳结构，最终证明了归并排序的正确性。此方法突出了形式化证明在算法设计中的重要性。