排序算法之：循环不变式在快速排序中的正确性证明 题目描述：使用循环不变式证明快速排序算法的正确性。具体来说，需要明确定义快速排序分区过程中的循环不变式，并证明在分区过程的初始化、保持和终止三个阶段中，该不变式始终成立，从而确保分区操作的正确性。 解题过程： 快速排序分区过程回顾 快速排序的核心是分区操作。以第一个元素为基准，将数组分为两部分：左边部分的所有元素小于等于基准，右边部分的所有元素大于基准。分区过程使用双指针法实现。 定义循环不变式 对于数组A[ p..r ]的分区过程，我们定义循环不变式为： 在每次循环开始时，对于某个基准元素A[ p ]，数组被划分为四个区域： A[ p ]：基准元素（最终位置待定） A[ p+1..i ]：所有元素 ≤ 基准 A[ i+1..j-1 ]：所有元素 > 基准 A[ j..r ]：尚未处理的元素 其中i指向最后一个≤基准的元素，j指向当前正在处理的元素。 证明循环不变式的正确性 初始化阶段： 在循环开始前，i = p，j = p+1 A[ p ]是基准元素 A[ p+1..i ]为空（因为i=p，区间长度为0） A[ i+1..j-1 ]为空（因为j=p+1，区间长度为0） A[ j..r ]包含除基准外的所有元素 此时，四个区域都满足定义，不变式成立。 保持阶段： 假设在第k次迭代时不变式成立，考虑第k+1次迭代： 情况1：如果A[ j ] ≤ 基准 将i右移一位，交换A[ i]和A[ j ]，然后j右移一位 这样操作后： A[ p+1..i]仍然都≤基准（新增的A[ i ]≤基准） A[ i+1..j-1 ]仍然都>基准（边界调整后保持不变） 处理了一个新元素A[ j ] 情况2：如果A[ j ] > 基准 只需将j右移一位 这样操作后： A[ p+1..i ]保持不变（都≤基准） A[ i+1..j-1 ]扩大，但仍保持都>基准 处理了一个新元素A[ j ] 两种情况下，不变式都得以保持。 终止阶段： 当j > r时循环结束，此时： A[ p ]是基准元素 A[ p+1..i ]都≤基准 A[ i+1..r ]都>基准 最后，将基准元素A[ p]与A[ i ]交换，使得： A[ p..i-1 ]都≤基准 A[ i ]就是基准元素的最终位置 A[ i+1..r ]都>基准 这就完成了正确的分区操作。 结论 通过循环不变式的证明，我们确保了快速排序分区过程的正确性。结合递归调用，整个快速排序算法能够正确地将数组排序。这个证明方法不仅适用于标准的快速排序，也可以推广到各种变体版本。