使用循环不变量证明堆排序的正确性答案

【问题标题】：Using loop invariants to prove the correctness of heap sort使用循环不变量证明堆排序的正确性
【发布时间】：2023-12-08 06:21:02
【问题描述】：

什么是循环不变量，如何使用它们来证明堆排序算法的正确性？

【问题讨论】：

【解决方案1】：

循环不变量是非常简单但功能强大的技术，可以证明您的算法或一组指令是否正确。它们在迭代中工作得非常好。

我们设置了一个不变的属性，这是您希望在整个执行过程中维护的迭代中的所需属性。例如，如果你从一个正确的状态开始并在整个算法过程中保持它，那么你就知道你有一个正确的算法

所以你需要证明你有一个想要的属性，3个步骤的不变性：

我。 初始化：你能证明你在循环迭代的第一步中具有算法的不变性吗？

二。维护：您是否在维护不变性？如果到那时为止的迭代是真的，那么下一次迭代也是真的吗？

iii.终止：当您的循环最终终止时，不变量将用于表明您编写的算法是正确的。

让我们用这些知识来证明 BuildMaxHeap 是正确的，因为它用于 HeapSort 算法。

BuildMaxHeap(A)
  heap-size[A] = length[A]
   for i : length[A]/2 to 1
       Max-Heapify(A, i)

来源。 CLRS

例如，我们怎么知道构建最大堆实际上是构建最大堆！如果我们的 BuildMaxHeap 算法正常工作，我们可以使用它来正确排序。

根据上述直觉，我们需要决定在整个算法中维护的所需属性。 MaxHeap 中所需的属性是什么？堆[i]>= 堆[i*2]。不管你怎么弄乱堆，如果它仍然有那个属性，那么它就是一个 MaxHeap。

因此，我们需要确保用于排序的 BuildMaxHeap 算法在整个算法中保持不变。

初始化：在第一次迭代之前。一切都是叶子，所以它已经是堆了。

维护：让我们假设到目前为止我们有一个可行的解决方案。节点 i 的子节点编号高于 i。 MaxHeapify 也保留了循环不变量。我们在每一步都保持不变性。

终止：当 i 下降到 0 时终止，并且通过循环不变量，每个节点都是最大堆的根。

因此您编写的算法是正确的。

Introduction to Algorithms (CLRS) 对这种技术有很好的处理。

【讨论】：

对于初始化，“一切都是一片叶子”怎么样？我太慢了，我已经读了一个小时了
i = floor(n/2) 是最后一个内部节点（非叶节点），否则 left = 2i 和 right = 2i + 1 会超过 n。因此， floor(n/2) + 1, ..., n 都是外部节点（叶节点）。例如，如果 n = 11，则 floor(11/2) + 1 = 6。6 不能有孩子，因为 left = 6*2 = 12，而 right 6*2 + 1 = 13 没有意义，因为 n = 11.

【解决方案2】：

循环不变量是在循环执行期间不会改变的“法则”。
在堆排序中——不变量是每个节点都具有堆属性——即节点中的值大于其左右子节点的值。

【讨论】：

【解决方案3】：

BuildMaxHeap 的正确性

•循环不变量： 在 for 循环的每次迭代开始时，每个节点 i+1、i+2、...、n 都是最大堆的根。

•初始化：——在第一次迭代之前 i= ⎣n/2⎦ – 节点 ⎣n/2⎦+1, ⎣n/2⎦+2, ..., n 是叶子，因此是平凡最大堆的根。

•维护：——根据 LI，节点 i 的子节点的子树是最大堆。 – 因此，MaxHeapify(i) 将节点 i 呈现为最大堆根（同时保留更高编号节点的最大堆根属性）。 – 递减 i 为下一次迭代重新建立循环不变量。

【讨论】：