An Assertional Proof of the Stability and Correctness of Natural Mergesort

  • Rustan Leino ,
  • Paqui Lucio

ACM Transactions on Computational Logic (TOCL) | , Vol 17(1)

View Publication

We present a mechanically verified implementation of the sorting algorithm commonly known as Natural Mergesort. The implementation consists in a few methods specified in the contract style of pre- and post-conditions. In addition, methods are annotated with assertions that, both, explain how it works, and allows the automatic verification of the contract satisfaction. This program-proof is made using the state-of-the-art verifier Dafny. We verify not only the standard sortedness condition of the algorithm, but also that it performs a stable sort. Along the paper we provide |and explain| the complete text of the program-proof.