Lean formalization of insertion sort stability and correctness

František Silváši, Martin Tomášek

Lean formalization of insertion sort stability and correctness

Číslo: 2/2018
Periodikum: Acta Electrotechnica et Informatica
DOI: 10.15546/aeei-2018-0015

Klíčová slova: Formal specification; Insertion sort; Proof of correctness; Theorem proving

Pro získání musíte mít účet v Citace PRO.

Přečíst po přihlášení

Anotace: We present a fully mechanized proof of correctness and stability of the insertion sort algorithm, while handling stability not as an afterthought in its formal specification, but rather as a property removing any unspecified behaviour from the algorithm, by explaining what happens to elements that are considered equivalent. We therefore express the combined notion of being sorted along with stability as a single inductive predicate, allowing us to share uncovered information in proofs, resulting in a more elegant approach to showing correctness and stability of sorting algorithms. Naturally, there are also cases when we can indeed forget about stability. We prove, that under the assumption that the sequence to be sorted contains unique elements only, sorting and stable sorting are equivalent notions. Formalization is conducted in the Lean theorem prover.