Durante la lettura di Introduction to Algorithms (3a edizione, P188), c'è un algoritmo chiamato Tail-Recursive-QuickSort e dobbiamo dimostrare la correttezza di questo algoritmo.
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
Il problema è che, quando ho provato ad utilizzare l'invariante di loop, ho trovato difficile per me spiegare chiaramente la manutenzione a causa della funzione ricorsiva all'interno del corpo del loop. Il ciclo invariante che utilizzo è:
Before each iteration, A[0:p-1] are sorted.
Il caso iniziale è banale, ma la manutenzione implica dimostrare che TAIL-RECURSIVE-QUICKSORT non cambia l'invarianza del ciclo. C'è un modo per spiegarlo chiaramente?
Grazie.