Using loop invariants to prove the correctness of heap sort

What are loop invariants and how do I 开发者_C百科use them to prove the correctness of the heap sort algorithm?

---

Loop Invariants are very simple yet powerful techniques to prove if your algorithm or a set of instruction is correct. They work wonderfully in iterations.

We set up an invariant property, which is a desired property in your iterations that you would want to maintain throughout the execution. For example if you started off with a correct state and maintained it throughout the course of algorithm, then you know that you have a correct algorithm

So you would need to show that you have a desired property, the invariance in 3 steps:

i. Initialization: Can you show that you have the invariant property of the algorithm in the first step of the iteration of the loop?

ii. Maintenance: Are you maintaining the invariance? If it was true for the iteration up to that point, is it true for the next iteration?

iii.Termination: When your loop finally terminates, the invariant will be used to show that the algorithm you wrote is correct.

Let us use this knowledge to prove BuildMaxHeap is correct, since it is used in the HeapSort algorithm.

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

Source. CLRS

For example, How do we know that building of max heap actually builds a max heap! If our BuildMaxHeap algorithm worked correctly, we could use this to sort correctly.

Following our above intuition, we need to decide on a desired property that we maintain throughout the algorithm. What is the desired property in the MaxHeap? heap[i]>= heap[i*2]. No matter how much you mess around with the heap, if it still has that property, then it is a MaxHeap.

So we need to make sure that our BuildMaxHeap algorithm used for the sorting maintains that invariant throughout the algorithm.

Initialization : Prior to the first iteration. Everything is a leaf so it is already a heap.

Maintainence : Let us assume that we have a working solution till now. The children of node i are numbered higher than i. MaxHeapify preserves the loop invariant as well. We maintain the invariance at each step.

Termination : Terminates when the i drops down to 0 and by the loop invariant, each node is the root of a max-heap.

Hence the algorithm you wrote is correct.

Introduction to Algorithms (CLRS) has a very good treatment of this technique.

---

Loop invariant is a 'Law' that does not change during the execution of the loop.
In heap sort - The invariant is that every node has the heap property - that is, the value in the node is bigger than the values of its left and right children.

---

Correctness of BuildMaxHeap

•Loop Invariant: At the start of each iteration of the for loop, each node i+1, i+2, ..., n is the root of a max-heap.

•Initialization:–Before first iteration i= ⎣n/2⎦ –Nodes ⎣n/2⎦+1, ⎣n/2⎦+2, ..., n are leaves, hence roots of trivial max-heaps.

•Maintenance: –By LI, subtrees at children of node i are max heaps. –Hence, MaxHeapify(i) renders node i a max heap root (while preserving the max heap root property of higher-numbered nodes). –Decrementing i reestablishes the loop invariant for the next iteration.