✍ Scribed by Jean-Christophe Filliâtre
No coin nor oath required. For personal study only.
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.
📜 SIMILAR VOLUMES
This article presents the design of a new functional 2D image segmentation algorithm by cell merging in a subdivision, its proof of total correctness, and the derivation of an optimal imperative program. The planar subdivisions are modeled by hypermaps. The formal specifications of hypermaps and seg