We present a mechanically verified implementation of the sorting algorithm  Natural Mergesort  that consists of a few methods specified by their contracts of pre/post conditions. Methods are annotated with assertions that allow 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 property, but also that the algorithm performs a stable sort. Throughout the article, we provide and explain the complete text of the program-proof.
['K. Rustan M. Leino', 'Paqui Lucio']
An Assertional Proof of the Stability and Correctness of Natural Mergesort