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 |