coq-hoare-tut

A Tutorial on Reflecting in Coq the generation of Hoare proof obligations. 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.5.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.5 & < 8.6~)
source
https://github.com/coq-contribs/hoare-tut/archive/v8.5.0.tar.gz
package
https://github.com/coq/opam-coq-archive/tree/master/released/packages/coq-hoare-tut/coq-hoare-tut.8.5.0