Efficiency and proof of patience sort algorithms compared in two systems
Certification of Bilateral Patience Sort in Theorema and Rocq
Logic in Computer Science
Summary
Sorting algorithms help organize data, but making sure they work correctly can be tricky. The authors studied a particular version of a sorting method called Patience Sort, improving it from a slow version to a faster one. They then used two different computer systems, Theorema and Rocq, to formally prove that these algorithms work as intended. Their comparison shows how different tools and ways of designing algorithms affect the ease of proving correctness.
What this means in practice
- •For software verification teams: Formalize and certify sorting algorithms to ensure their correctness in critical software systems.
- •For formal method tool developers: Use insights on algorithm design and proof complexity to improve proof assistant capabilities for complex algorithms.
Authors
Isabela Drǎmnesc, Tudor Jebelean, Sorin Stratulat
Abstract
This is a case study on a specific version of the Patience Sort algorithm in which we illustrate the evolution of it from an intuitive but inefficient nested recursion into a more complex but more efficient tail recursion, together with its formal implementation and certification in Theorema and Rocq (formerly Coq). We identify some general principles of algorithm transformation, and we develop the necessary background theory and proof methods. As a significant distinctive aspect, the approach in Theorema uses multisets, which simplifies the whole process and makes it more intuitive. The certification process reveals significant differences between the Theorema and Rocq approaches, about which we provide a comparative analysis with respect to algorithm definition, proof development, and proof effort. This analysis offers insights into how algorithm design influences the complexity and structure of formal proofs and demonstrates how non-trivial algorithms can be effectively verified across different formal frameworks.