排序算法之：循环不变式在冒泡排序中的正确性证明 题目描述：使用循环不变式来证明冒泡排序算法的正确性。冒泡排序是一种简单的排序算法，它重复地遍历要排序的数列，一次比较两个元素，如果它们的顺序错误就把它们交换过来。遍历数列的工作是重复地进行直到没有再需要交换，也就是说该数列已经排序完成。 解题过程： 理解循环不变式 循环不变式是用于证明算法正确性的一种形式化方法。它是指在循环的每次迭代开始和结束时都为真的一个条件。对于排序算法，我们通常关心的是在循环的特定点，数组的某个部分已经处于正确的状态。 定义冒泡排序算法 我们首先明确标准的冒泡排序算法（以升序排序为例）： 输入：一个包含 n 个元素的数组 A 。 输出：按非降序排列的数组 A 。 过程： 设置一个外部循环，从 i = 0 到 i = n-2 （共 n-1 轮遍历）。 在每一轮 i 中，设置一个内部循环，从 j = 0 到 j = n-i-2 。 在内部循环中，比较相邻元素 A[j] 和 A[j+1] 。如果 A[j] > A[j+1] ，则交换它们的位置。 这个算法的核心思想是，每一轮外部循环都会将当前未排序部分中的最大元素“冒泡”到其正确的位置（即未排序部分的末尾）。 为冒泡排序建立循环不变式 对于冒泡排序，一个关键的循环不变式是关于外部循环的。我们这样定义循环不变式 P(i) ： 陈述 ：在外部循环的第 i 次迭代 之后 ，数组 A 中 最后 i 个元素 （即子数组 A[n-i] 到 A[n-1] ）不仅包含了整个数组中最大的 i 个元素，并且它们已经位于其最终的正确排序位置上。 初始情况 (i=0) ：在外部循环开始之前（即第0次迭代之后）， i=0 。最后0个元素是空集。空集自然满足“包含了最大的0个元素且已排序”的条件。因此， P(0) 为真。这被称为 初始化 。 保持情况 ：我们需要证明，如果循环不变式在一次迭代之前为真，那么在下一次迭代之后它仍然为真。这就是 保持 。 假设在外部循环的第 k 次迭代 之后 ， P(k) 为真。即，数组的最后 k 个元素（ A[n-k] 到 A[n-1] ）是最大的 k 个元素且已排好序。 现在考虑第 k+1 次迭代。这次迭代的内部循环从 j=0 遍历到 j=n-k-2 。内部循环的任务是在当前未排序的部分（ A[0] 到 A[n-k-1] ）中找到最大的元素。 通过相邻元素的比较和交换，这个最大的元素会像“气泡”一样一步步地被交换（“冒泡”）到未排序部分的末尾，即位置 A[n-k-1] 。 此时，位置 A[n-k-1] 上的元素就是整个数组中第 (k+1) 大的元素（因为最后 k 个位置已经是最大的 k 个元素，所以当前找到的是剩下的元素中最大的）。 因此，在第 k+1 次外部迭代 之后 ，子数组 A[n-k-1] 到 A[n-1] 包含了最大的 k+1 个元素，并且它们已经排好序（ A[n-k-1] 是第 k+1 大，其后的 k 个元素是更大的且已排好序）。所以 P(k+1) 为真。 这就证明了循环不变式的保持性。 终止 循环不变式在循环终止时给出了一个非常有用的性质，这帮助我们证明算法的正确性。 外部循环在 i 从 0 递增到 n-1 时终止（实际执行了 n-1 次）。 当 i = n-1 时，根据循环不变式 P(n-1) ：数组的最后 n-1 个元素是最大的 n-1 个元素且已排好序。 此时，整个数组只剩下第一个元素 A[0] 没有被循环不变式明确覆盖。但是，既然最大的 n-1 个元素都已经在它们正确的位置上，那么剩下的唯一一个元素 A[0] 必然是最小的元素，并且它就应该在第一个位置。因此，整个数组 A[0..n-1] 都已经按升序排列。 通过以上步骤—— 初始化 、 保持 、 终止 ——我们严格地证明了冒泡排序算法的正确性。循环不变式清晰地描述了算法在每一步所维持的逻辑状态，是理解算法行为的有力工具。