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

Question

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

Answer 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) 对这种技术有很好的处理。