Contribution: HoareTut

A Tutorial on Reflecting in Coq the generation of Hoare proof obligations

Authors

Description

This work is both an introduction to Hoare logic and a demo illustrating Coq nice features. It 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.

Keywords

hoare logic, imperative program, weakest precondition, reflection

README

***************************
* Tutorial on Hoare Logic *
***************************

-----
 A Tutorial on Reflecting in Coq the generation of Hoare proof obligations
-----

-----
 Copyright 2007 Sylvain Boulme
-----

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).

-----
 Short description
-----

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.

 
-----
 Aims of this library
-----

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.

-----
 How to read the sources
-----

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.

-----
 Contact
-----

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

Available files