排序算法之：循环不变式在 Strand Sort 中的正确性证明 题目描述 Strand Sort 是一种基于归并和提取的排序算法，其核心思想是反复从原列表中提取已排序的“ strands”（连续递增子序列），并将这些 strands 归并到一个新列表中，直到原列表为空。题目要求通过循环不变式（Loop Invariant）严格证明 Strand Sort 的正确性，即算法执行过程中每一步都保持关键性质，最终得到完整排序的数组。 解题过程 理解 Strand Sort 的基本步骤 初始状态：未排序的输入列表 A ，空的结果列表 B 。 循环过程： a. 从 A 中提取一个 strand（从左到右扫描，依次选取比前一个元素大的元素，保持相对顺序）。 b. 将新提取的 strand 与 B 归并（类似归并排序的合并操作）。 c. 重复直到 A 为空。 定义循环不变式 设第 k 次循环结束后： 不变式 1 ：结果列表 B 始终是排序的。 不变式 2 ： B 中的元素是原列表 A 中已处理部分的全局有序子集。 不变式 3 ： A 中剩余元素均大于等于 B 的最后一个元素（若 B 非空），保证后续归并不会破坏 B 的有序性。 初始状态验证 初始时 B 为空，视为已排序，不变式 1 和 2 成立。 由于 B 为空，不变式 3 无条件成立。 循环保持性证明 提取 strand ：新 strand 是从 A 中按顺序提取的递增序列，故其自身有序。 归并操作 ：将有序的 strand 与有序的 B 归并，结果 B' 仍有序（不变式 1 保持）。 元素关系 ：归并时，strand 的首元素必然不小于 B 的末元素（由提取规则和不变式 3 保证），因此归并后 B' 的末元素是当前全局最大值，剩余 A 中的元素均不小于它（不变式 3 保持）。 终止条件与正确性 当 A 为空时，循环终止。此时所有元素已转移到 B ，且由不变式 1 知 B 有序，故算法正确。 复杂度分析（补充说明） 最坏情况：每次仅提取一个元素（如逆序数组），需 O(n) 次归并，每次归并 O(n) ，总复杂度 O(n²) 。 优化方向：通过并行提取多个 strands 或优化归并策略提升效率（如使用平衡归并树）。 总结 通过循环不变式严格证明了 Strand Sort 的每一步都保持结果列表有序且逐步包含全局有序元素，最终得到正确排序。此方法适用于分析其他基于增量归并的排序算法。