coq-hoare-tut

A Tutorial on Reflecting in Coq the generation of Hoare proof obligations. http://www-verimag.imag.fr/~boulme/HOARE_LOGIC_TUTORIAL/ 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.

opam install coq-hoare-tut.8.7.0
homepage
https://github.com/coq-contribs/hoare-tut
license
GNU LGPL
bugs tracker
https://github.com/coq-contribs/hoare-tut/issues
dependencies
coq (>= 8.7 & < 8.8~)
source
https://github.com/coq-contribs/hoare-tut/archive/v8.7.0.tar.gz
package
https://github.com/coq/opam-coq-archive/tree/master/released/packages/coq-hoare-tut/coq-hoare-tut.8.7.0