Chapter 18: Proof of imperative programs
Jean-Christophe Filliātre
This chapter describes a new tactic
to prove the correctness and termination of imperative
programs annotated in a Floyd-Hoare logic style.
This tactic is provided in the Coq module Programs,
which does not belong to the initial state of Coq. So you must import
it when necessary, with the following command:
Require Programs.
If you want to use this tactic with the native-code version of Coq,
you will have to run the version of Coq with all the tactics, through
the command
coqtop -full
Be aware that this tactic is still very experimental.