排序算法之：循环不变式在计数排序中的正确性证明 题目描述 计数排序是一种非比较的整数排序算法，其核心思想是通过统计每个元素出现的次数，然后计算每个元素在输出数组中的正确位置。本题要求使用循环不变式（Loop Invariant）来严格证明计数排序算法的正确性，确保排序后的数组满足非递减顺序。 解题过程 1. 算法步骤回顾 计数排序包含三个主要步骤（假设输入数组为 A[0..n-1] ，元素范围为 [0, k] ）： 计数阶段 ：创建辅助数组 C[0..k] ，其中 C[i] 记录元素 i 在 A 中出现的次数。 前缀和阶段 ：对 C 进行前缀和计算，使 C[i] 表示小于等于 i 的元素个数。 放置阶段 ：从后向前遍历 A ，根据 C 中记录的位置信息，将元素放入输出数组 B 的正确位置。 2. 定义循环不变式 我们重点关注 放置阶段 的循环不变式。假设放置阶段循环变量为 j （从 n-1 递减到 0 ），输出数组为 B[0..n-1] ，前缀和数组为 C[0..k] 。循环不变式定义为： 不变式条件 ：在每次循环开始时，对于任意元素 x ， B 中已放置的元素（即 B 中索引大于 C[x] 的位置）均大于 x ，且 B 中索引小于等于 C[x] 的位置可能包含小于等于 x 的元素，但尚未放置完毕。 更形式化的描述 ： 对于所有 x ， B[0..C[x]-1] 中的元素均小于等于 x （但可能未填满）。 对于所有 x ， B[C[x]..n-1] 中的元素均大于 x （且已放置完毕）。 3. 初始化证明 在循环开始前（ j = n-1 ），输出数组 B 为空。此时： 对于任意 x ， B[0..C[x]-1] 为空，满足“元素均小于等于 x ”的条件（空集自然成立）。 B[C[x]..n-1] 为空，满足“元素均大于 x ”的条件。 ✅ 不变式在初始化时成立。 4. 保持证明 假设在循环的某次迭代开始时（ j = i ），不变式成立。本次迭代处理元素 A[i] ： 查找 A[i] 应放的位置： pos = C[A[i]] - 1 （因为 C[A[i]] 表示小于等于 A[i] 的元素个数，所以最后一个 A[i] 应放在 pos 位置）。 将 A[i] 放入 B[pos] 。 更新 C[A[i]] 减1，表示下一个 A[i] （如果存在）应放在更前的位置。 为什么不变式保持？ 放置前，根据不变式， B[pos+1..n-1] 中的元素均大于 A[i] （因为 pos+1 > C[A[i]]-1 ）。 放置后， B[pos] 被设为 A[i] ，而 B[0..pos-1] 中的元素均小于等于 A[i] （由 C 的前缀和性质保证）。 更新 C[A[i]] 后，对于其他元素 y ≠ A[i] ， C[y] 未变，因此关于 y 的不变式条件不受影响。 ✅ 不变式在迭代后仍然成立。 5. 终止证明 当循环结束时（ j = -1 ），所有元素已放入 B 。此时不变式表明： 对于任意元素 x ， B[0..C[x]-1] 中的元素均小于等于 x ，且 B[C[x]..n-1] 中的元素均大于 x 。 但由于所有元素已放置，且 C[x] 最终值为 x 的最小可能位置（因为 C 被递减更新），实际上 B 中所有小于等于 x 的元素恰好占据 B[0..C[x]-1] ，而大于 x 的元素占据后续位置。因此 B 整体有序。 ✅ 算法正确性得证。 关键点总结 循环不变式将动态的放置过程与静态的有序性关联起来。 前缀和数组 C 的更新保证了相同元素的稳定性（从后向前遍历确保先出现的元素放在后面）。 通过分析初始化、保持和终止三个阶段，完整证明了计数排序的正确性。