J.-C. Filliātre. Formal Proof of a Program: Find. Science of Computer Programming, 2001. To appear.

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 hand-made proof, where the program is given together with its formal specification and where each step is fully justified by a 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 establishing the total correctness of imperative programs. We follow Hoare's paper as close 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 reasonings 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.

[ bib | .ps.gz ]

Back