Argue the correctness of \(\textsc{Heapsort}\) using the following loop invariant:
At the start of each iteration of the for loop of lines 2–5, the subarray \(A[1..i]\) is a max-heap containing the \(i\) smallest elements of \(A[1..n]\), and the subarray \(A[i+1..n]\) contains the \(n-i\) largest elements of \(A[1..n]\), sorted.
To prove the correctness of heapsort, we need to verify that the loop invariant holds at three critical points: initialization, maintenance, and termination. This standard technique for proving algorithm correctness ensures that the invariant provides a useful property when the loop completes.
Initialization
Before the first iteration of the for loop, \(i = A.\textit{length} = n\). At this point, the subarray \(A[1..n]\) is a max-heap (established by the call to \(\textsc{Build-Max-Heap}\) in line 1), which trivially contains the \(n\) smallest elements of the original array. The subarray \(A[n+1..n]\) is empty, so it trivially contains zero elements in sorted order. Thus, the invariant holds prior to the first iteration.
Maintenance
To see that each iteration maintains the loop invariant, consider what happens during an iteration with loop index \(i\). At the start, by the loop invariant, \(A[1..i]\) is a max-heap containing the \(i\) smallest elements, and \(A[i+1..n]\) contains the \(n-i\) largest elements in sorted order.
The key observation is that the maximum element in \(A[1..i]\) (which is \(A[1]\) by the max-heap property) must be the largest among the \(i\) smallest elements. Furthermore, since \(A[i+1..n]\) contains the \(n-i\) largest elements and these are all larger than anything in \(A[1..i]\), we know that \(A[1]\) is exactly the \(i\)-th smallest element overall.
In line 3, we exchange \(A[1]\) with \(A[i]\), placing this \(i\)-th smallest element in position \(i\). In line 4, we decrement \(A.\textit{heap-size}\), effectively removing position \(i\) from the heap. Now \(A[i..n]\) contains the \(n-i+1\) largest elements.
After the exchange, the new root \(A[1]\) might violate the max-heap property, but the children of the root are still roots of max-heaps. Therefore, \(\textsc{Max-Heapify}(A, 1)\) in line 5 restores the max-heap property for \(A[1..i-1]\). This subarray now contains the \(i-1\) smallest elements as a max-heap.
For the sorted portion, since the element we just placed at position \(i\) is smaller than all elements in \(A[i+1..n]\) (because those are the \(n-i\) largest elements), and we placed the largest remaining element at position \(i\), the subarray \(A[i..n]\) is sorted. Decrementing \(i\) reestablishes the loop invariant for the next iteration.
Termination
The loop terminates when \(i = 1\). At this point, by the loop invariant, \(A[1..1]\) is a max-heap containing the 1 smallest element (which is just the minimum element), and \(A[2..n]\) contains the \(n-1\) largest elements in sorted order. Since the single element in \(A[1]\) must be smaller than all elements in \(A[2..n]\), the entire array \(A[1..n]\) is sorted in increasing order.