3

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

4

3 回答 3

8

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

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

所以你需要证明你有一个想要的属性，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 中所需的属性是什么？堆[i]>= 堆[i*2]。不管你怎么弄乱堆，如果它仍然有那个属性，那么它就是一个 MaxHeap。

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

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

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

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

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

算法简介（CLRS）对这种技术有很好的处理。

于 2010-12-06T09:44:42.367 回答
1

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

于 2010-12-06T09:29:39.977 回答
0

BuildMaxHeap 的正确性

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

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

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

于 2017-01-20T03:12:39.283 回答