我开始研究计算逻辑，作为练习，我想证明归并排序算法的正确性。
目前，我很难证明该算法的输出将始终对应于给定输入的排列。
如果有人能帮我解决这个问题，我会很高兴。
非常感谢????
【问题讨论】：
标签： algorithm sorting mergesort divide-and-conquer correctness
这个证明的核心需要证明“合并”过程将每个元素插入一次且仅一次插入结果中。由于合并过程使用循环工作，因此您需要使用loop invariant 来显示这一点。
循环不变量通常可以通过询问“我知道什么中途循环？”来发现？
to merge arrays A and B:
let n = length of A, m = length of B
let R = new array of length (n + m)
let i = 0, j = 0
while i < n or j < m:
if i < n and (j == m or A[i] <= B[j]):
R[i+j] = A[i]
i = i + 1
else:
R[i+j] = B[j]
j = j + 1
return R
在这个循环中，我们总是知道 R 的前 i+j 个元素是 A 的前 i 个元素和 B 的前 j 个元素的某种排列。这就是循环不变量，所以你需要证明：
一般而言，此类证明的难点在于发现循环不变量，并表明循环的每次迭代都保留了不变量。
【讨论】：
归并排序的前提是什么？什么是岗位条件？你有任何循环不变量吗？
在您开始编写证明之前，您必须问自己三个问题。
那么：您的基本情况是什么？如果您正在处理证明，大概您知道合并排序是如何工作的，那么当您将一个长度为 1 的数组传递给合并排序函数时会发生什么？那里的后置条件是什么？
这里有一个decent primer from Berkeley，关于如何证明函数的正确性。编写证明可能需要一些离散数学（归纳）。
【讨论】：