algorithm - 使用Loop不变式证明合并排序的正确性(初始化，维护，终止)

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

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

多谢!

最佳答案

合并排序的伪代码

MERGE-SORT(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)

MERGE-SORT(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

我们尝试对两堆卡片进行排序，但是在每个基本步骤中我们都避免检查任一堆卡片是否为空，因此我们将infinite用作哨兵卡片来简化代码。因此，无论何时暴露前哨卡无限，除非两个桩都都暴露了前哨卡，否则它不可能是较小的卡。但是一旦发生这种情况，所有非哨兵卡都已经放置在输出桩上。由于我们已经预先知道将r - p + 1卡准确地放置在输出堆上，因此我们可以在执行了许多基本步骤后停止。

循环不变量:

初始化:在循环的第一次迭代之前，我们有k = p，因此子数组A[p ... k - 1]为空。此空子数组包含L和R的k - p = 0最小元素，并且由于i = j = 1，L [i]和R [j]都是其数组中尚未复制回A的最小元素。

维护:要看到每个迭代都保持循环不变，让我们首先假设l [i] 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])按排序顺序包含k - p = r - p + 1和L[1 ... n1 + 1]的R[1 ... n2 + 1]最小元素。数组L和R一起包含n1 + n2 + 2 = r - p + 3元素。除了两个最大元素之外的所有元素都已复制回A，并且这两个最大元素是前哨。

关于algorithm - 使用Loop不变式证明合并排序的正确性(初始化，维护，终止)，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/40499805/