Quicksort
General Information
Algorithmic problem: Sorting based on pairwise comparison
Type of algorithm: recursion
Abstract View
Invariant: After a recursive call, the input sequence of this recursive call is sorted.
Variant: In each recursive call, the sequence of the callee is strictly shorter than that of the caller.
Break condition: The sequence is empty or a singleton.
Induction Basis
Abstract view: Nothing to do on an empty sequence or a singleton.
Implementation: Ditto.
Proof: Empty sequences and singletons are trivially sorted.