Using loop invariants to prove the correctness of heap sort

Question

What are loop invariants and how do I use them to prove the correctness of the heap sort algorithm?

Answer 1

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.