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 |