循环不变式在快速排序中的正确性证明 题目描述：使用循环不变式（Loop Invariant）来证明快速排序（QuickSort）算法的正确性。快速排序是一种基于分治策略的排序算法，其核心操作是分区（Partition），通过选择基准元素将数组划分为两个子数组，使得左子数组的元素均小于等于基准，右子数组的元素均大于等于基准。循环不变式用于形式化证明分区过程的正确性，确保排序结果的正确性。 解题过程循序渐进讲解： 快速排序算法概述 快速排序的基本步骤： 选择基准元素（pivot），例如数组的第一个元素、最后一个元素或随机元素。 分区操作：重新排列数组，使得所有小于等于基准的元素位于基准左侧，大于等于基准的元素位于右侧。分区后，基准元素处于其最终排序位置。 递归地对左右两个子数组进行快速排序。 示例：对数组 [5, 2, 9, 3, 7] 进行排序，选择最后一个元素 7 为基准，分区后可能得到 [5, 2, 3, 7, 9] ，然后递归排序左子数组 [5, 2, 3] 和右子数组 [9] 。 分区过程的循环不变式定义 分区是快速排序的关键，我们使用循环不变式来证明其正确性。以 Lomuto 分区方案为例（选择最后一个元素为基准）： 初始化：设数组为 A[p..r] ，基准为 A[r] 。定义两个指针： i 表示“小于等于基准区域的边界”，初始时 i = p - 1 ； j 为当前遍历指针，初始时 j = p 。 循环不变式：在每次迭代开始时，对于任意索引 k ： 如果 p ≤ k ≤ i ，则 A[k] ≤ pivot （小于等于基准的区域）。 如果 i + 1 ≤ k ≤ j - 1 ，则 A[k] > pivot （大于基准的区域）。 如果 k = r ，则 A[k] = pivot （基准元素本身）。 维护：在循环的每次迭代中，检查 A[j] ： 如果 A[j] ≤ pivot ，则交换 A[i+1] 和 A[j] ，然后递增 i 。这扩展了小于等于基准的区域。 如果 A[j] > pivot ，则仅递增 j ，扩展大于基准的区域。 终止：当 j = r 时循环结束。此时，所有元素已被处理。最后，交换 A[i+1] 和 A[r] ，将基准放置到正确位置。此时， A[p..i] 均 ≤ pivot， A[i+2..r] 均 > pivot，而 A[i+1] 是基准。 循环不变式的正确性证明 初始化：在循环开始时， i = p - 1 ， j = p 。小于等于基准的区域为空（因为 p ≤ k ≤ i 无有效索引），大于基准的区域也为空（ i+1 ≤ k ≤ j-1 无有效索引）。不变式成立。 维护：假设迭代前不变式成立。根据 A[j] 的值： 若 A[j] ≤ pivot ：交换后， A[i+1] （原大于基准区域的第一个元素）被换为 A[j] （≤ pivot），同时 i 增加，扩展了小于等于基准的区域。 j 增加后，原 A[j] 被纳入大于基准区域（因其被交换到位置 i+1 ，但此时 i 已更新，区域边界调整）。 若 A[j] > pivot ：仅增加 j ，直接扩展大于基准的区域。 每次操作后，不变式保持不变。 终止：当 j = r 时，所有元素已处理。根据不变式： A[p..i] 均 ≤ pivot。 A[i+1..r-1] 均 > pivot（因 j-1 = r-1 ）。 交换 A[i+1] 和 A[r] 后，基准被放置到位置 i+1 ，此时 A[p..i] ≤ pivot， A[i+1] 是基准， A[i+2..r] > pivot。分区正确。 结合快速排序的递归过程 分区正确性保证基准元素处于最终位置。递归排序左右子数组时，对子数组应用相同的分区和循环不变式证明。 基础情况：当子数组长度 ≤ 1 时，自然有序。 通过数学归纳法，整个数组最终被正确排序。 总结：循环不变式形式化验证了分区操作的可靠性，从而确保快速排序的正确性。这种方法可扩展到其他分区方案（如 Hoare 分区），只需调整不变式定义。