When I was reading Introduction to Algorithms (3rd edition, P188), there is an algorithm called Tail-Recursive-QuickSort and we have to prove the correctness of this algorithm.
TAIL-RECURSIVE-QUICKSORT(A, p, r) 1 while p < r 2 // Partition and sort left subarray. 3 q = PARTITION(A, p, r) 4 TAIL-RECURSIVE-QUICKSORT(A, p, q - 1) 5 p = q + 1
The problem is, when I tried to use loop invariant, I found it difficult for me to explain the maintenance clearly because of the recursive function inside the loop body. The loop invariant I use is:
Before each iteration, A[0:p-1] are sorted.
The initial case is trivial, but the maintenance involves prove TAIL-RECURSIVE-QUICKSORT doesn't change loop invariant. Is there any way to explain it clearly?