Formal Verification of Sorting Correctness: Heap Sort and Invariant Induction

FORMAL VERIFICATION OF SORTING CORRECTNESS: HEAP SORT AND INVARIANT INDUCTION Heap Sort is a comparison-based sorting algorithm with a deterministic time complexity of O(N log N) and in-place memory usage. Proving its correctness formally requires verifying two sequential phases: building the binary heap (heapification) and extracting elements in sorted order. These proofs are established using loop invariants. THE BINARY HEAP INVARIANT A binary max-heap is a complete binary tree where the key stored at each node is greater than or equal to the keys stored at its children: Parent(i) >= Child(i) For an array representation of a binary tree, the children of node "i" reside at indices 2i + 1 and 2i + 2. PHASE 1: HEAPIFICATION CORRECTNESS The heapify operation restores the max-heap invariant for a subtree. Loop Invariant: At the start of each iteration of the loop that builds the heap, every node at a level deeper than the current index is the root of a valid max-heap. Proving the invariant: - Initialization: The loop starts at the lowest non-leaf nodes. Since leaf nodes contain no children, they are trivially valid max-heaps. - Maintenance: If the subtrees of node "i" are valid max-heaps, running heapify on node "i" compares it with its children, swapping if necessary, and recursively heapifies the affected subtree. This maintains the invariant for node "i". - Termination: The loop terminates when index reaches the root (0), establishing that the entire binary tree satisfies the max-heap invariant. PHASE 2: SORTING CORRECTNESS Once the max-heap is constructed, the sorting loop repeatedly swaps the root element (index 0, the maximum value) with the last element of the heap, decrements the active heap size, and runs heapify on the root. Loop Invariant: At the start of each iteration of the sorting loop, the subarray from index N-k to N-1 contains the k largest elements of the input array in sorted ascending order, and the subarray from 0 to N-k-1 forms a valid max-heap. Through structural induction on the loop counter, this invariant proves that when the heap size reaches 1, the entire array is sorted. Reference: Yang Hu, "Algorithms Python.pdf", Chapter 24: Binary Heap Sorting.