Argue the correctness of \(\textsc{Heap-Increase-Key}\) using the following loop invariant:
At the start of each iteration of the while loop of lines 4–6, \(A[\textsc{Parent}(i)] \geq A[\textsc{Left}(i)]\) and \(A[\textsc{Parent}(i)] \geq A[\textsc{Right}(i)]\), if these nodes exist, and the subarray \(A[1 \,.\,. A.\text{heap-size}]\) satisfies the max-heap property, except that there may be one violation: \(A[i]\) may be larger than \(A[\textsc{Parent}(i)]\).
You may assume that the subarray \(A[1 \,.\,. A.\text{heap-size}]\) satisfies the max-heap property at the time \(\textsc{Heap-Increase-Key}\) is called.
To prove correctness using a loop invariant, we must establish three properties: initialization (the invariant is true before the first iteration), maintenance (if true before an iteration, it remains true before the next), and termination (when the loop ends, the invariant gives us a useful property).
The key insight is that \(\textsc{Heap-Increase-Key}\) maintains the heap property everywhere except possibly at one position (node \(i\)), and each iteration moves this potential violation one level closer to the root.
Initialization
Before the first iteration of the while loop, line 3 has set \(A[i] = \text{key}\), where \(\text{key} \geq A[i]\) (the old value). Since the heap satisfied the max-heap property before this assignment, all nodes except possibly \(i\) still satisfy the property.
Node \(i\) now has a larger key, which might make it larger than its parent, potentially violating the max-heap property. However, since we only increased \(A[i]\), we did not affect the relationship between \(\textsc{Parent}(i)\) and its children. If \(\textsc{Parent}(i)\) has children other than \(i\) (or if \(i\) itself has children), those relationships remain valid because we only changed \(A[i]\), not any other nodes.
Therefore, the invariant holds before the first iteration: the heap is valid except that \(A[i]\) may exceed \(A[\textsc{Parent}(i)]\).
Maintenance
Assume the invariant holds at the start of an iteration. We must show it holds at the start of the next iteration.
If the loop condition \(i > 1\) and \(A[\textsc{Parent}(i)] < A[i]\) is true, then we have a violation at position \(i\). The loop body (lines 5–6) swaps \(A[i]\) with \(A[\textsc{Parent}(i)]\) and sets \(i = \textsc{Parent}(i)\).
After the swap:
-
The old parent position (now containing the larger value that was at \(i\)) satisfies the max-heap property with respect to its children. The old \(i\) position now contains a smaller value, and any other children of the old parent remain smaller than the parent (by the invariant assumption). Thus, the old parent’s relationships are valid.
-
The new position \(i\) (which is the old parent position) now contains the larger value. This might violate the max-heap property with respect to its parent, but all other heap relationships remain valid.
-
All other nodes in the heap are unaffected by the swap, so their heap relationships remain valid.
Therefore, after updating \(i\), the invariant holds for the next iteration: the heap is valid except that \(A[i]\) may exceed \(A[\textsc{Parent}(i)]\).
Termination
The loop terminates when either \(i = 1\) (we’ve reached the root) or \(A[\textsc{Parent}(i)] \geq A[i]\) (the heap property is satisfied at position \(i\)).
In both cases, the max-heap property holds throughout the entire array:
- If \(i = 1\), node \(i\) is the root and has no parent, so there’s no violation.
- If \(A[\textsc{Parent}(i)] \geq A[i]\), the potential violation has been eliminated.
By the invariant, all other positions already satisfied the heap property. Therefore, when the loop terminates, the entire array \(A[1 \,.\,. A.\text{heap-size}]\) satisfies the max-heap property.