排序算法之：循环不变式在 Cocktail Sort 中的正确性证明 题目描述 Cocktail Sort（鸡尾酒排序）是冒泡排序的一种变体，它通过双向交替遍历数组来改善冒泡排序的性能。具体来说，算法先从左到右遍历，将最大元素移动到右侧正确位置；然后从右到左遍历，将最小元素移动到左侧正确位置。如此反复，直到数组完全有序。本题要求证明 Cocktail Sort 的正确性，即通过循环不变式（Loop Invariant）严格证明算法执行过程中关键性质始终成立，并最终导致数组有序。 解题过程 1. 算法步骤回顾 Cocktail Sort 的核心步骤如下（以升序排序为例）： 步骤1 ：设置左右边界 left = 0 ， right = n-1 （n 为数组长度）。 步骤2 ：从左到右遍历 [left, right] ，比较相邻元素，若逆序则交换，将最大元素移至 right 位置。 步骤3 ：将 right 减 1。 步骤4 ：从右到左遍历 [left, right] ，比较相邻元素，若逆序则交换，将最小元素移至 left 位置。 步骤5 ：将 left 加 1。 步骤6 ：重复步骤2~5，直到 left >= right 。 2. 定义循环不变式 循环不变式是证明正确性的关键工具。对于 Cocktail Sort，我们定义以下两个循环不变式，分别对应双向遍历的每一轮： 从左到右遍历后 ： 设当前右边界为 r ，则子数组 [r+1, n-1] 已有序，且 [r+1, n-1] 中的元素均大于等于 [0, r] 中的任意元素。 从右到左遍历后 ： 设当前左边界为 l ，则子数组 [0, l-1] 已有序，且 [0, l-1] 中的元素均小于等于 [l, n-1] 中的任意元素。 3. 初始化阶段 初始时 left = 0 ， right = n-1 。 在第一次从左到右遍历前， [right+1, n-1] 即 [n, n-1] 为空，不变式自然成立。 类似地，第一次从右到左遍历前， [0, left-1] 即 [0, -1] 为空，不变式也成立。 4. 保持阶段 假设在第 k 轮迭代中： 从左到右遍历 ： 遍历区间 [left, right] ，通过相邻比较交换，确保遍历结束后 arr[right] 是 [left, right] 中的最大值。因此： [right+1, n-1] 仍保持有序（因之前操作已保证）。 新增的 arr[right] 小于等于 [right+1, n-1] 的最小值（因 arr[right] 是 [left, right] 的最大值，而 [right+1, n-1] 的最小值来自之前的 [left, right] 范围）。 故不变式 [right+1, n-1] 有序且整体最大值得以保持。 从右到左遍历 ： 遍历区间 [left, right] ，通过相邻比较交换，确保遍历结束后 arr[left] 是 [left, right] 中的最小值。因此： [0, left-1] 仍保持有序。 新增的 arr[left] 大于等于 [0, left-1] 的最大值（类似理由）。 故不变式 [0, left-1] 有序且整体最小值得以保持。 5. 终止阶段 当 left >= right 时循环结束。此时： 由最后一次从左到右遍历的不变式， [right+1, n-1] 有序且整体最大。 由最后一次从右到左遍历的不变式， [0, left-1] 有序且整体最小。 由于 left >= right ，区间 [left, right] 至多包含一个元素（或为空），该元素自然有序。 因此整个数组 [0, n-1] 有序。 6. 总结 通过循环不变式，我们严格证明了 Cocktail Sort 在每轮双向遍历后均能扩大已排序的子数组范围，并保证已排序部分与未排序部分之间的数值大小关系。最终，当左右边界相遇时，整个数组被划分为三个有序部分（左已排序、中间单元素、右已排序），且中间元素与左右部分的大小关系一致，因此数组完全有序。