排序算法之：循环不变式在 Gnome Sort 中的正确性证明

题目描述
Gnome Sort（地精排序）是一种简单的排序算法，其核心思想是通过相邻元素的比较和交换，逐步将元素移动到正确的位置。算法从数组的起始位置开始，每次比较当前元素与前一个元素，如果顺序错误则交换它们，并后退一步；如果顺序正确则前进一步。这个过程重复直到整个数组有序。现在，要求使用循环不变式（Loop Invariant）来严格证明 Gnome Sort 的正确性。

解题过程
我们将通过定义循环不变式、验证其初始和终止状态，并分析每次迭代后的状态变化，来证明算法的正确性。

1. 算法步骤回顾
   Gnome Sort 的伪代码如下：

   index = 0
   while index < length(array):
       if index == 0 or array[index] >= array[index - 1]:
           index += 1
       else:
           swap array[index] and array[index - 1]
           index -= 1
   

   • 算法从 index = 0 开始遍历数组。
   • 如果当前元素大于等于前一个元素（或处于起始位置），则前进（index += 1）。
   • 否则，交换当前元素与前一个元素，并后退（index -= 1）。

2. 定义循环不变式
   循环不变式是：在每次循环迭代开始时，子数组 array[0..index-1] 是有序的。

   • 这里 array[0..index-1] 表示从索引 0 到 index-1 的元素（左闭右开区间）。
   • "有序" 指非降序排列，即对于任意 i（0 ≤ i < index-1），有 array[i] ≤ array[i+1]。

3. 证明循环不变式的正确性

   • 初始状态：
     当第一次进入循环时，index = 0，子数组 array[0..-1] 为空。空数组默认是有序的，因此循环不变式成立。

   • 保持状态：
     假设在某个迭代开始时，循环不变式成立（即 array[0..index-1] 有序）。我们分析两种情况：

     • 情况 1：index == 0 或 array[index] ≥ array[index-1]。
       此时不进行交换，直接执行 index += 1。
       由于原 array[0..index-1] 有序，且 array[index]（新位置的当前元素）大于等于前一个元素，因此 array[0..index] 保持有序。循环不变式在迭代后依然成立。
     • 情况 2：array[index] < array[index-1]。
       执行交换操作：将 array[index] 和 array[index-1] 交换，然后 index -= 1。
       交换后，array[index-1]（原 array[index]）可能小于其前一个元素，但通过后退一步，算法会重新检查并调整这个位置。关键点在于：交换操作确保了较大的元素被移动到右侧，而通过后续的迭代，算法会逐步将较小的元素“冒泡”到左侧正确位置。由于每次交换都减少了逆序对的数量，并且循环不变式在调整过程中逐步恢复，因此整体有序性得以保持。

   • 终止状态：
     当循环结束时，index = length(array)。根据循环不变式，此时 array[0..length(array)-1] 有序，即整个数组已排序。

4. 边界情况与效率分析

   • 边界处理：当 index = 0 时，算法直接前进，避免非法访问。
   • 时间复杂度：最坏情况下（如完全逆序数组），Gnome Sort 的时间复杂度为 O(n²)，但通过循环不变式可证明其必然终止且结果正确。

总结
通过循环不变式，我们严格证明了 Gnome Sort 在每次迭代中维护了子数组的有序性，最终使得整个数组排序正确。这种方法不仅适用于 Gnome Sort，还可推广到其他类似交换排序算法的正确性分析中。