This file is part of the "Tutorial on Hoare Logic". The "Tutorial on Hoare Logic" is a Coq library distributed under the terms of the "GNU LESSER GENERAL PUBLIC LICENSE" version 3. For further details, see http://www.gnu.org/licenses/gpl-3.0.txt and http://www.gnu.org/licenses/lgpl-3.0.txt.
Hoare logics are "program logics" suitable for reasoning about imperative programs. This library formalizes the generation of PO (proof obligations) in a Hoare logic for a very basic imperative programming language. It proves the soundness and the completeness of the PO generation both in partial and total correctness. At last, it examplifies on a very simple example (a GCD computation) how the PO generation can simplify concrete proofs. Coq is indeed able to compute PO on concrete programs: we say here that the generation of proof obligations is reflected in Coq. Technically, the PO generation is here performed through Dijkstra's weakest-precondition calculus.
This work is both an introduction to Hoare logic and a demo illustrating Coq nice features. Indeed, the power of Coq higher order logic allows to give a very simple description of Hoare logic. Actually, I find this presentation simpler than those found in some hand-written books. In particular, because we are in a rich language, some notions which are not in the "kernel" of the logic (e.g. the return types of expressions or the assertion language) can be simply "shallow embedded": we do need to introduce an abstract syntax for these notions, and we can handle directly their semantics instead. Furthermore, because Coq is a programming language with propositions as first class citizens, it is able to compute the PO of Hoare logic on concrete imperative programs. At last, most of proofs in this development are discharged by Coq, using only a few hints given by the user. Most of these hints are simply some key ideas of the proofs.
In summary, this work aims to illustrate the following ideas:
I use this library in some talks presenting Coq. It takes me usually between 45 minutes and 1 hour to present its different part.
The best way to read the sources is to read them through coqide (or your favorite coq interface): you will be able to replay the (short) proofs of this development. In particular, replaying proof of gcd_partial_proof and gcd_total_proof in file exgcd.v allows to see how Coq generates PO on a concrete example. To do so, you may first need to download the sources and then to compile them using make. Alternatively, you can browse the html documentation through your favorite web browser. In case of trouble, please contact me.
To read the sources, you may follow this order:
If you have any comment, suggestion, question or trouble about this work, please send a mail to Sylvain.Boulme@imag.fr
For more information, see my web page at http://www-verimag.imag.fr/~boulme