使用循环不变量证明归并排序的正确性（初始化、维护、终止）

Question

你将如何通过对循环不变量状态的推理来证明合并排序的正确性？我唯一可以想象的是在合并步骤中，子数组（不变量）在组合时保持它们的状态，即它们在每次合并时再次排序 step.But 我不知道我是否进行正确或 not.I 对循环不变量没有太多了解 stuff.Can 有人启发我这个？。解释每个阶段会发生什么

a) 初始化 b) 维护 c) 终止

感激不尽！

Answer 1

合并排序的伪代码

合并排序(A, p, r)

    1 if p < r
    2    then q <-- [(p + r) / 2]
    3          MERGE-SORT(A, p, q)
    4          MERGE-SORT(A, q + 1, r)
    5          MERGE-SORT(A, p, q, r)

合并排序（A、p、q、r）

    1  n1 <-- q - p + 1 
    2  n2 <-- r - q
    3  create arrays L[1 ... n1 + 1] and R[1 ... n2 + 1]
    4  for i <-- 1 to n1
    5       do L[i] <-- A[p + i - 1]
    6  for j <-- 1 to n2
    7      do R[j] <-- A[q + j]
    8  L[n1 + 1] <-- infinite 
    9  R[n2 + 1] <-- infinite
    10 i <-- 1
    11 j <-- 1
    12 for k <-- p to r
    13     do if L[i] <= R[j]
    14           then A[k] <-- L[i]
    15                i <-- i + 1
    16           else A[k] <-- R[j]
    17                j <-- j + 1

我们尝试对两堆卡片进行排序，但我们避免在每个基本步骤中检查任一堆是否为空，并且我们使用无限作为哨兵卡片来简化我们的代码。所以，无论什么时候哨兵卡 infinie 被暴露出来，它都不可能是较小的牌，除非两堆的哨兵牌都暴露了。但是一旦发生这种情况，所有非哨兵卡都已经放在输出堆上了。因为我们事先知道 r - p + 1 张卡片将被放入输出堆，所以我们可以在执行完那么多基本步骤后停止。

循环不变量：
- 初始化：在循环的第一次迭代之前，我们有 k = p，因此子数组 A[p ... k - 1] 为空。此空子数组包含 L 和 R 的 k - p = 0 个最小元素，并且由于 i = j = 1，L[i] 和 R[j] 都是其数组中尚未复制回 A 的最小元素.
- 维护：要看到每次迭代都保持循环不变，让我们首先假设 l[i] <= R[j]。那么 L[i] 是尚未复制回 A 的最小元素。因为 A[p ... k - 1] 包含 k - p 个最小元素，在第 14 行将 L[i] 复制到 A[k] 后，子数组 A[p ... k] 将包含 k - p + 1 个最小的元素。递增 k（在 for 循环更新中）和 i（在第 15 行）为下一次迭代重新建立循环不变量。相反，如果 L[i] > R[j]，则第 16-17 行执行适当的操作以保持循环不变。
- 终止：终止时，k = r + 1。根据循环不变式，子数组 A[p ... k - 1] 即 A[p ... r] 包含 L[1 ... n1 + 1] 和 R[1 ... n2 + 1] 的最小元素 k - p = r - p + 1，按排序顺序排列。数组 L 和 R 一起包含 n1 + n2 + 2 = r - p + 3 个元素。除了两个最大的元素之外的所有元素都被复制回 A，这两个最大的元素是哨兵。

使用循环不变量证明归并排序的正确性（初始化、维护、终止）

Using Loop invariant to prove correctness of merge sort (Initialization , Maintenance , Termination)

algorithm

loops

sorting

mergesort

invariants