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

Question

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

Answer 1

Loop Invariants是非常简单但功能强大的技术,用于证明您的算法或一组指令是否正确.它们在迭代中运行得非常好.

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

因此,您需要通过3个步骤显示您具有所需属性,不变性:

一世.初始化:你可以在循环迭代的第一步显示你有算法的不变属性吗？

II.维护:您是否保持不变性？如果到那时的迭代是真的,那么下一次迭代是否属实？

III.终止:当你的循环终止时,不变量将用于表明你编写的算法是正确的.

让我们使用这些知识来证明BuildMaxHeap是正确的,因为它在HeapSort算法中使用.

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

资源.CLRS

例如,我们怎么知道最大堆的构建实际上构建了一个最大堆!如果我们的BuildMaxHeap算法正常工作,我们可以使用它来正确排序.

遵循我们的上述直觉,我们需要决定我们在整个算法中维护的所需属性.MaxHeap中所需的属性是什么？heap [i]> = heap [i*2].无论你在堆中乱七八糟,如果它仍然具有该属性,那么它就是MaxHeap.

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

初始化:在第一次迭代之前.一切都是叶子,所以它已经是一堆.

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

终止:当i下降到0并且循环不变时终止,每个节点都是最大堆的根.

因此,您编写的算法是正确的.

算法简介(CLRS)对此技术有很好的处理.