关于插入排序外层循环不变式维护阶段一致性的技术问询

背景回顾 #

我正在阅读CLRS所著《算法导论》中插入排序的循环不变式相关内容，插入排序的伪代码如下：

1 for i = 2 to n
2   key = A[i]
3   // Insert A[i] into the sorted subarray A[1:i-1]
4       j = i -1
5       while j>0 and A[j] > key
6           A[j+1] = A[j]
7           j = j-1
8       A[j + 1] = key

外层for循环的循环不变式正式定义为：在第1-8行for循环的每次迭代开始时，子数组A[1:i-1]包含原本A[1:i-1]中的元素且已排序。

为证明算法正确性，需验证循环不变式在三个阶段均成立：

• 初始化：i=2时，子数组A[1:1]仅含原元素A[1]且有序，满足循环不变式。
• 维护：for循环体通过移动A[i-1]、A[i-2]等元素找到A[i]的正确位置并插入，使A[1:i]成为原元素的有序子数组，之后i递增进入下一次循环。
• 终止：i增至n+1时，代入循环不变式得A[1:n]为原元素的有序子数组，算法正确。

核心疑问 #

证明算法正确性的核心是验证每次迭代开始时A[1:i-1]已排序，但维护阶段实际将排序范围扩展到了A[i]，这是否与外层循环不变式的正式定义一致？

解答 #

完全一致，这正是循环不变式维护阶段的核心逻辑：

1. 迭代开始时，我们依赖不变式保证A[1:i-1]是有序的原元素子数组；
2. 循环体的移动元素、插入key操作，正是基于这个有序子数组，将A[i]插入到正确位置，让A[1:i]成为新的有序原元素子数组；
3. 当i递增后，下一次迭代开始时，新的i对应的A[1:i-1]就是上一轮的A[1:i]，自然满足循环不变式的要求。

简言之，维护阶段的“扩展排序范围”就是为了让下一次迭代的不变式依然成立——它是不变式从当前迭代传递到下一次迭代的桥梁，完全契合不变式的定义逻辑。

内容的提问来源于stack exchange，提问作者novice