13 lines
521 B
Plaintext
13 lines
521 B
Plaintext
A simple formulation of Hoare logic for a WHILE-language, with a proof of /relative completeness/:
|
|
|
|
If a triple { P } s { Q } is valid in the model, then it is derivable
|
|
using the rules in Hoare.v (see the inductive type `hoare_triple`).
|
|
|
|
Requires std++: <https://gitlab.mpi-sws.org/iris/stdpp>.
|
|
(Tested with git version f8719169e3ed75123d88c59d292ddd0972351ad3).
|
|
|
|
|
|
BEWARE!!! I wrote this formalization when I started my PhD, and I
|
|
didn't know much about (idiomatic) Coq back then. As a result, the
|
|
code is quite shitty.
|