Argue the correctness of HEAPSORT using the following loop invariant:
At the start of each iteration of the for loop on 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.
Initialization: Immediately prior to the first iteration of the loop we perform BUILD-MAX-HEAP on our heap and the subarray A[1…i] is in fact the entire heap because i=n. Therefore A[1…i] trivially contains the i smallest elements of A, and A[i+1…n] is empty.
Maintenance: Each iteration of the for loop decrements i by 1 after shifting the largest element from A[i…1] to A[i+1…n]. Because we are always shifting the largest element, it must be true that only the smallest elements remain in A[1…i]. Likewise, A[i+1…n] represents the n−i elements that have already been shifted and so must contain the largest elements of A in increasing order.
Termination: The loop terminates when i=1 at which point A[1…i] contains one element: the smallest element of A. In addition, we have shifted n−1 elements into A[2…n] which are the n−1 largest elements of A in increasing order. Thus A is sorted.