排序算法之：循环不变式在快速排序中的正确性证明 题目描述 使用循环不变式（Loop Invariant）来证明快速排序（QuickSort）在划分（Partition）过程中的正确性。具体来说，需要证明在划分过程的每一步中，数组元素都能被正确地重新排列，使得所有小于主元（pivot）的元素位于主元左侧，所有大于主元的元素位于主元右侧。 解题过程 理解划分过程的目标 快速排序的划分步骤选取一个主元（例如数组最后一个元素），并重新排列数组，使得： 主元被放置到其最终排序位置。 主元左侧的所有元素 ≤ 主元。 主元右侧的所有元素 ≥ 主元。 循环不变式需确保这一目标在划分过程中逐步达成。 定义循环不变式 在划分算法的循环中（例如Lomuto划分方案），定义以下不变式： 设数组区间为 [low, high] ，主元为 arr[high] 。 循环变量 i 表示当前小于等于主元的子数组的末尾索引（初始为 low-1 ）。 循环变量 j 用于遍历数组（初始为 low ）。 循环不变式 ： 对于任意索引 k ： 若 low ≤ k ≤ i ，则 arr[k] ≤ pivot 。 若 i+1 ≤ k ≤ j-1 ，则 arr[k] > pivot 。 若 k = high ，则 arr[k] = pivot （主元未被移动）。 区间 [j, high-1] 为尚未处理的元素。 初始状态验证 初始时 i = low-1 ， j = low 。 区间 [low, i] 为空，满足“所有元素 ≤ pivot”。 区间 [i+1, j-1] 为空（因为 j-1 = low-1 ），满足“所有元素 > pivot”。 区间 [j, high-1] 包含全部待处理元素。 结论 ：循环不变式在初始状态下成立。 循环迭代维护不变式 遍历过程中，对于每个 j ： 情况1 ：若 arr[j] ≤ pivot ，则 i 增加1，交换 arr[i] 和 arr[j] 。 交换后， arr[i] （原 arr[j] ）≤ pivot，区间 [low, i] 仍满足条件。 原 arr[i] （交换后位于 j ）可能 > pivot，但此时 j 已递增，该元素被纳入区间 [i+1, j-1] （大于pivot的区间）。 情况2 ：若 arr[j] > pivot ，仅递增 j 。 元素 arr[j] 自动落入区间 [i+1, j-1] （大于pivot的区间）。 主元始终位于 high 未被移动。 结论 ：每次迭代后，不变式仍然保持成立。 终止条件与正确性 循环终止时 j = high ，此时区间 [j, high-1] 为空，所有元素已处理。 根据不变式： [low, i] 的元素 ≤ pivot。 [i+1, high-1] 的元素 > pivot。 最后交换 arr[i+1] 和 arr[high] ，将主元放置到正确位置 i+1 。 最终数组满足： [low, i] ≤ pivot， arr[i+1] = pivot ， [i+2, high] ≥ pivot。 结论 ：划分正确性得证。 总结 循环不变式通过明确循环各阶段的元素状态，确保了划分过程的正确性。这一方法可推广至其他排序算法的证明中，强调算法设计中不变式的重要性。