Dafny Code for Variations on Quicksort
Recursive Quicksort
Dafny-code for a recursive version of quicksort.
(Lemmas used but not proven.)
Iterative Quicksort - Initialisation and Finalisation
Dafny-code for the iterative, pivot-based version of quicksort.
We only prove that the initialization establishes the invariant, and that the then part preserves the invariant.
(Lemmas used but not proven.)
Iterative Quicksort - Invariant Preservation
Dafny-code for the iterative, pivot-based version of quicksort.
We only prove that the else part preserves the invariant.
(Lemmas used but not proven.)