An Assertional Proof of the Stability and Correctness of Natural Mergesort

We present a mechanically verified implementation of the sorting algorithm commonly known as Natural Mergesort. The imple-mentation consists in a few methods specified in the contract style of pre- and post-conditions. In addition, methods are annotated with as-sertions that, both, explain how it works, and allows the automatic verifi-cation of the contract satisfaction. This program-proof is made using the state-of-the-art verifier Dafny. We verify not only the standard sorted-ness 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