Formal proof of a program: Find

In 1971, C.A.R. Hoare gave the proof of correctness and termination of a rather complex algorithm, in a paper entitled Proof of a program: Find. It is a handmade proof, where the program is given together with its formal specification and where each step is fully justified by mathematical reasoning. We present here a formal proof of the same program in the system Coq, using the recent tactic of the system developed to establish the total correctness of imperative programs. We follow Hoare’s paper as closely as possible, keeping the same program and the same specification. We show that we get exactly the same proof obligations, which are proved in a straightforward way, following the original paper. We also explain how more informal aspects of Hoare’s proof are formalized in the system Coq. This demonstrates the adequacy of the system Coq in the process of certifying imperative programs.