the generation of Hoare proof obligations

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.

This library requires Coq version 8.1 (Feb. 2007).

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:

- Coq is suitable both for reasoning about program logics and for emulating these logics.
- Reflecting Dijkstra's weakest-precondition calculus is an elegant and powerful way to reason about non-functional programs in Coq.

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:

- Start by reading hoarelogicsemantics.v (the semantics of my Hoare logic) and exgcd.v (which examplifies how to use this Hoare logic). It seems a good idea to read these files more or less in parallel.
- Then, read partialhoarelogic.v the PO generation in partial correctness.
- At last, read totalhoarelogic.v the PO generation in total correctness. Indeed, the PO generation in total correctness may be considered as a refinement of the PO generation in partial correctness.
- It seems almost useless to read hoarelogic.v. Its purpose is only to glue all this stuff together.

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