LEAN FORMALIZATION OF INSERTION SORT STABILITY AND CORRECTNESS
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...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Sciendo
2018-02-01
|
| Series: | Acta Electrotechnica et Informatica |
| Online Access: | http://www.aei.tuke.sk/papers/2018/2/06_Silvasi.pdf |
| Summary: | 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. |
|---|---|
| ISSN: | 1335-8243 1338-3957 |