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

Question

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

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

我们尝试对两堆卡片进行排序，但我们避免在每个基本步骤中检查任一堆是否为空，我们使用无限作为标记牌来简化我们的代码。所以，每当哨卡无限被暴露时，它不能是较小的卡，除非两堆都暴露了他们的哨卡。但是一旦发生这种情况，所有非哨兵卡都已经被放置到输出堆中。由于我们事先知道确切的r - p + 1卡片将被放置到输出堆中，因此一旦我们执行了这么多基本步骤，我们就可以停止。

• 循环不变量：

  • 初始化：在循环的第一次迭代之前，我们有k = p，所以子数组A[p ... k - 1]是空的。这个空的子数组包含k - p = 0L 和 R的最小元素，因为i = j = 1，L[i] 和 R[j] 都是它们数组中没有被复制回 A 的最小元素。

  • 维护：为了看到每次迭代都保持循环不变，让我们首先假设 l[i] <= R[j]。那么 L[i] 是尚未复制回 AA[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]，包含k - p = r - p + 1的最小元素L[1 ... n1 + 1]，并R[1 ... n2 + 1]在排序顺序。数组 L 和 R 一起包含n1 + n2 + 2 = r - p + 3元素。除了两个最大的元素外，所有元素都被复制回 A，这两个最大的元素是哨兵。