6.4-2

Argue the correctness of 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.
Initialization: when i = A.length A[1 ..A.length] is a max- heap as we use build-max-heap containing A.length smallest elements of A[1 ..A.length] and A[i+1..n] will contain zero elements. Maintenance: For each iteration by the loop invariant A[1..i] will contain i smallest elements of A[1..n]. After iteration i the largest element of max-heap will be exchanged with A[i] and A[1..i] will contain i smallest elements of A[1..n]. Line 3 of the procedure exchanges A[1] with A[i] making A[i..n] n-i+1 largest elements of A[1..n]. The heapsize is reduced (heapsize = i -1). No the subarray A[1..i-1] is a not max heap.The root violates the max heap property but child obey the property. We call Max-heapify to make A[1..i-1] a max heap. Termination: when i = 1 we have subarray containing A[2..n] n-i+1 largest elements of A[1..n] and A[1..i] containing the smallest element of A[1..n].