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

我将为你详细讲解 Strand Sort 算法，并重点阐述如何通过循环不变式来证明其正确性。Strand Sort 是一种基于归并策略的排序算法，其核心思想是从初始列表中依次提取已排序的“ strands ”（ strand 意为“股”或“串”），然后将这些有序的 strands 归并成一个完整的有序列表。

题目描述

问题：给定一个包含 n 个元素的未排序列表，请使用 Strand Sort 算法对其进行升序排序，并利用循环不变式严格证明该算法的正确性。

算法核心步骤简述：

1. 初始化一个空的结果列表，用于存放最终排序好的元素。
2. 只要原始输入列表不为空，就重复以下过程：
   a. 从原始列表中提取一个有序的 strand。这个 strand 的提取规则是：从原始列表的剩余元素中，依次找出不小于当前 strand 最后一个元素的元素，将其从原始列表移除并加入到当前 strand 中。
   b. 将这个新提取出的有序 strand 与已有的结果列表进行归并（类似于归并排序中的合并步骤）。
3. 当原始列表为空时，结果列表即为排序后的列表。

我们的目标是证明，经过有限次迭代后，此算法确实能产生一个完全有序的列表。

解题过程：循序渐进的讲解

我们将证明过程分解为几个关键步骤，并引入循环不变式作为核心工具。

步骤 1：深入理解 Strand Sort 算法流程

在证明之前，我们必须精确理解算法。以下是 Strand Sort 的伪代码：

function strandSort(inputList):
    resultList = [] // 步骤1：初始化空的结果列表
    while inputList is not empty: // 步骤2：主循环
        // 2a. 提取一个有序strand
        sublist = []
        // 总是从inputList的第一个未处理元素开始
        move the first element from inputList to sublist
        i = 0
        while i < length(inputList):
            if inputList[i] >= last element of sublist:
                move inputList[i] from inputList to sublist
            else:
                i = i + 1

        // 2b. 将有序strand (sublist) 归并到结果列表 (resultList) 中
        resultList = merge(resultList, sublist)

    return resultList

// 归并两个已排序列表的函数
function merge(listA, listB):
    mergedList = []
    i = 0, j = 0
    while i < length(listA) and j < length(listB):
        if listA[i] <= listB[j]:
            append listA[i] to mergedList
            i = i + 1
        else:
            append listB[j] to mergedList
            j = j + 1
    // 将剩余元素追加到mergedList
    append the rest of listA (from index i) to mergedList
    append the rest of listB (from index j) to mergedList
    return mergedList

关键观察：

• 每次迭代提取的 sublist 本身都是有序的（非递减）。
• merge 函数接收两个有序列表，并产出一个新的有序列表。

步骤 2：定义循环不变式

循环不变式是证明算法正确性的强大工具。对于 Strand Sort 的主循环（while inputList is not empty），我们定义以下循环不变式：

循环不变式：在每一次主循环迭代开始时，resultList 都是一个有序的列表。并且，resultList 中包含了所有此前已经从 inputList 中移除的元素。

让我们详细解释这个不变式：

1. 有序性：resultList 始终保持升序排列。
2. 内容完整性：resultList 包含了所有已经被处理过的元素，没有遗漏。
3. 时机：这个性质在每次循环迭代之前（即循环条件 inputList is not empty 被检查时）都必须成立。

步骤 3：证明循环不变式的三个性质

一个有效的循环不变式必须满足三个性质：初始化、保持和终止。

性质一：初始化（Initialization）

• 时机：在第一次主循环迭代开始之前。
• 状态：此时，resultList 被初始化为空列表 []。inputList 包含所有 n 个未排序的元素。
• 验证：
  • 一个空列表在技术上可以被认为是“有序的”（因为没有元素违反顺序）。
  • 空列表也确实包含了所有此前从 inputList 中移除的元素（因为尚未移除任何元素）。
• 结论：循环不变式在第一次迭代开始前成立。

性质二：保持（Maintenance）

• 时机：假设循环不变式在第 k 次迭代开始前成立，我们需要证明它在第 k+1 次迭代开始前也成立。
• 归纳假设：在第 k 次迭代开始时，resultList_(k) 是有序的，并且包含了所有此前移除的元素。
• 迭代过程：
  1. 提取 Strand：算法从 inputList 中提取出一个新的有序 strand，我们称之为 sublist_k。根据提取规则，sublist_k 本身是有序的。
  2. 归并操作：算法调用 merge(resultList_(k), sublist_k)。merge 函数的功能是：给定两个有序列表作为输入，它总是输出一个合并后的有序列表。这是一个被严格证明过的子程序正确性。
• 迭代结果：在第 k 次迭代结束后，resultList 被更新为 merge(resultList_(k), sublist_k) 的结果，我们称之为 resultList_(k+1)。由于 resultList_(k) 和 sublist_k 都是有序的，且 merge 操作正确，所以 resultList_(k+1) 也是有序的。
• 内容完整性：resultList_(k+1) 包含了 resultList_(k) 的所有元素和 sublist_k 的所有元素，即包含了至今所有从 inputList 中移除的元素。
• 结论：在第 k+1 次迭代开始前（也就是第 k 次迭代结束后），循环不变式仍然成立。不变式的“保持”性质得证。

性质三：终止（Termination）

• 时机：当主循环的条件 inputList is not empty 变为假时，循环终止。
• 终止状态：此时，inputList 为空。根据循环不变式，在最后一次循环迭代结束后（即循环终止时），resultList 是有序的。
• 最终结果：因为 inputList 为空，意味着原始列表中的所有元素都已经被移除并处理过了。根据循环不变式的内容完整性，这些所有元素现在都存在于有序的 resultList 中。
• 结论：因此，算法返回的 resultList 就是原始列表中所有元素构成的一个有序排列。算法正确。

步骤 4：补充说明与边界条件

• 有限性：算法一定会终止吗？是的。因为每次迭代至少会从 inputList 中移除一个元素（最开始的那个元素），而 inputList 初始大小为 n。所以最多经过 n 次迭代，inputList 必为空。
• 稳定性：Strand Sort 可以是稳定的。如果在 merge 函数中，当元素相等时，我们优先从 resultList（代表之前已处理的元素）中取元素，然后再从新的 sublist 中取，那么原始的顺序可以得到保持。
• 性能：虽然正确性得到保证，但 Strand Sort 的时间复杂度在最坏情况下可能达到 O(n²)，这发生在输入列表为逆序时，每次只能提取一个元素形成一个 strand。其性能严重依赖于输入数据的初始顺序。

总结

通过定义“结果列表始终有序且包含所有已处理元素”这一循环不变式，并严格证明其在初始化、保持和终止三个阶段的正确性，我们完整地证明了 Strand Sort 算法的正确性。这个证明过程清晰地展示了循环不变式如何帮助我们形式化地推理一个具有循环结构的算法的行为，确保其在任何合法输入下都能产生预期的输出。