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

题目描述：
桶排序（Bucket Sort）是一种分布式排序算法，它将元素分到有限数量的桶中，然后对每个桶单独排序，最后按顺序合并结果。我们将探讨如何用循环不变式严格证明桶排序的正确性。

解题过程：

1. 桶排序算法概述

   • 输入：包含n个元素的数组A，元素均匀分布在区间[0,1)
   • 步骤：
     a) 创建n个空桶（链表）
     b) 将每个元素A[i]放入桶⌊n·A[i]⌋中
     c) 对每个桶进行插入排序
     d) 按顺序连接所有桶

2. 循环不变式的定义
   我们需要证明两个关键循环的正确性：

   a) 元素分配循环：
   for i = 1 to n
   将A[i]插入桶B[⌊n·A[i]⌋]

   循环不变式：前i个元素已正确分配到对应的桶中

   b) 桶排序循环：
   for i = 0 to n-1
   对桶B[i]进行插入排序

   循环不变式：前i个桶已排序完成

3. 元素分配循环的正确性证明

   • 初始化：i=0时，没有元素被分配，条件成立
   • 保持：假设前i个元素已正确分配。处理第i+1个元素时，我们计算⌊n·A[i+1]⌋将其放入对应桶，分配正确
   • 终止：i=n时，所有元素都正确分配到桶中

4. 桶内排序的正确性证明

   • 每个桶使用插入排序，其循环不变式已证明正确
   • 关键观察：桶排序依赖于每个桶内排序的正确性

5. 整体正确性的关键证明点
   a) 顺序保持性：如果A[i] ≤ A[j]，则A[i]要么在A[j]的桶中，要么在编号更小的桶中
   b) 数学证明：设⌊n·A[i]⌋ = k，⌊n·A[j]⌋ = l

   • 若k < l，A[i]在A[j]之前输出
   • 若k = l，插入排序保证相对顺序

6. 边界情况处理

   • 空桶：直接跳过不影响结果
   • 单元素桶：自然有序
   • 全相同元素：都在同一桶中，插入排序保持稳定

7. 完整正确性证明
   通过数学归纳法证明：

   • 基础：空数组自然有序
   • 归纳：假设前k个桶已排序正确，考虑第k+1个桶
     • 桶k中的最大值 ≤ 桶k+1中的最小值（由分配规则保证）
     • 桶k+1内部有序（由插入排序保证）
     • 因此连接后整个序列有序

这个证明展示了桶排序如何通过分布策略和稳定排序的组合保证最终结果的有序性。