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 |
| _version_ | 1797762217487106048 |
|---|---|
| author | František SILVÁŠI Martin TOMÁŠEK |
| author_facet | František SILVÁŠI Martin TOMÁŠEK |
| author_sort | František SILVÁŠI |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-03-12T19:25:06Z |
| format | Article |
| id | doaj.art-c00bbff1d0524f138d30d9070ae52c7d |
| institution | Directory Open Access Journal |
| issn | 1335-8243 1338-3957 |
| language | English |
| last_indexed | 2024-03-12T19:25:06Z |
| publishDate | 2018-02-01 |
| publisher | Sciendo |
| record_format | Article |
| series | Acta Electrotechnica et Informatica |
| spelling | doaj.art-c00bbff1d0524f138d30d9070ae52c7d2023-08-02T04:57:26ZengSciendoActa Electrotechnica et Informatica1335-82431338-39572018-02-01182424910.15546/aeei-2018-0015LEAN FORMALIZATION OF INSERTION SORT STABILITY AND CORRECTNESSFrantišek SILVÁŠIMartin TOMÁŠEKWe 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.http://www.aei.tuke.sk/papers/2018/2/06_Silvasi.pdf |
| spellingShingle | František SILVÁŠI Martin TOMÁŠEK LEAN FORMALIZATION OF INSERTION SORT STABILITY AND CORRECTNESS Acta Electrotechnica et Informatica |
| title | LEAN FORMALIZATION OF INSERTION SORT STABILITY AND CORRECTNESS |
| title_full | LEAN FORMALIZATION OF INSERTION SORT STABILITY AND CORRECTNESS |
| title_fullStr | LEAN FORMALIZATION OF INSERTION SORT STABILITY AND CORRECTNESS |
| title_full_unstemmed | LEAN FORMALIZATION OF INSERTION SORT STABILITY AND CORRECTNESS |
| title_short | LEAN FORMALIZATION OF INSERTION SORT STABILITY AND CORRECTNESS |
| title_sort | lean formalization of insertion sort stability and correctness |
| url | http://www.aei.tuke.sk/papers/2018/2/06_Silvasi.pdf |
| work_keys_str_mv | AT frantiseksilvasi leanformalizationofinsertionsortstabilityandcorrectness AT martintomasek leanformalizationofinsertionsortstabilityandcorrectness |