Mechanical Verification of Insert-Sort and Merge-Sort Using Multisets in Theorema
Isabela Drămnesc, Tudor Jebelean · 2023
One important characteristic of environment re-search1is the handling of very large amounts of data, which can be only be achieved by organizing it in a highly efficient way, in particular by keeping various indexing lists in a sorted way and maintaining them efficiently. Therefore sorting algorithms that are specifically tailored to the various situations occurring in data acquisition, storage, and maintenance are crucial for systems that support advanced environment research, and they are useful only to the extent that they are correct. Checking the correctness of sorting algorithms, especially automatically, is a quite complex task. This paper introduces some special proof-based techniques for the automatic generation of correctness proofs of the algorithms Insert-Sort and Merge-Sort, including their auxiliary subfunctions, in the Theorema system. The proofs are described as they are generated by the system. This case study contributes in discovering novel proof-based techniques for algorithm verification and to the generalization of the techniques that authors have used for proof-based algorithm synthesis.