Built--Max-Heap正确性证明 At the start of each iteration of the for loop of lines 2-3,each node i+1. i+2.....nis the root of a max-heap. Initialization:Prior to the first iteration of the loop,i=n/2.Each node n/2+1.n/+2.....n is a leaf and is thus the root of a trivial max-heap. Maintenance:To see that each iteration maintains the loop invariant,observe that the children of node i are numbered higher than i.By the loop invariant,there- fore,they are both roots of max-heaps.This is precisely the condition required for the call MAX-HEAPIFY(A.i)to make node i a max-heap root.Moreover, the MAX-HEAPIFY call preserves the property that nodes i+1.i+2.....n are all roots of max-heaps.Decrementing i in the for loop update reestablishes the loop invariant for the next iteration. Termination:At termination,i=0.By the loop invariant,each node 1,2.....m is the root of a max-heap.In particular,node 1 is.Built-Max-Heap正确性证明