排序算法之：循环不变式在奇偶移排序（Odd-Even Transposition Sort）中的正确性证明

题目描述
奇偶移排序是一种基于比较的并行排序算法，适用于多处理器系统。其核心思想是通过交替的奇偶阶段比较交换相邻元素，逐步将最大值"冒泡"到正确位置。我们需要通过循环不变式严格证明该算法的正确性，并分析其边界条件处理。

解题过程

1. 算法原理回顾

   • 在奇数阶段（odd phase），比较所有奇数索引对 (1,2),(3,4),...,(2k-1,2k)
   • 在偶数阶段（even phase），比较所有偶数索引对 (2,3),(4,5),...,(2k,2k+1)
   • 每对元素若逆序则交换，重复 n/2 轮（n为数组长度）

2. 定义循环不变式
   对于第k轮排序后的数组a[0...n-1]：

   • 不变式P(k): 数组末尾的min(k, ⌈n/2⌉)个元素已处于最终有序位置
   • 更精确地说：经过m=2k-1次比较后，至少前⌊m/n⌋个最大元素已就位

3. 基础情况证明

   • 初始时k=0，数组末尾0个元素有序，P(0)成立
   • 完成第1轮（奇+偶阶段）后：
     • 奇数阶段将最大值移动到索引1,3,5...位置
     • 偶数阶段将该最大值继续向右传递至少1位
     • 最终最大值到达末尾，P(1)成立

4. 归纳步骤证明
   假设P(k)成立，证明P(k+1)：

   • 考虑第k+1轮的奇数阶段：
     • 由于前k轮已固定末尾k个元素，当前处理区间为a[0...n-k-1]
     • 奇数比较会将区间内最大值移动到奇数索引位置
   • 紧接着的偶数阶段：
     • 该最大值会通过偶数比较对继续向右移动
     • 由于末尾已排序元素形成"屏障"，最大值最终停在n-k-1位置
   • 因此新增一个元素到达最终位置，P(k+1)得证

5. 边界条件处理

   • 当n为奇数时，最后一个偶数阶段比较对为(n-2,n-1)
   • 当n为偶数时，最后一个奇数阶段需处理(n-2,n-1)对
   • 循环不变式在两种情况下均保持：
     • 通过min(n-i, n-j)限制比较范围
     • 使用⌊(n+1)/2⌋作为轮数上界

6. 终止条件证明

   • 经过⌈n/2⌉轮后，根据不变式：
     • 末尾⌈n/2⌉个元素已有序
     • 且这些元素包含整个数组的最大⌈n/2⌉个元素
     • 因此前⌊n/2⌋个元素自动有序
   • 最终整个数组有序，算法正确性得证

关键洞察
该证明揭示了奇偶移排序与冒泡排序的本质区别：通过奇偶交替比较，每个元素每两轮可移动最多两个位置，从而将时间复杂度保持在O(n²)但常数因子更优，特别适合并行实现。