First-order logic; a simple imperative language; Hoare triples. Rules for derivation; validity with respect to an operational semantics; soundness and completeness. Applications in program specification and verification; tools for formal verification; Design by Contract™ and lightweight verification.
Some questions I posed: why is the skip statement useful? Why might an axiomatic semantics not be enough? I also discussed what the soundness and completeness properties mean.
I didn’t show example use of the rules: a fun pen and paper exercise is to try to prove some of the example triples given using the Hoare rules and logic. This may be more intricate than you expect!
Read the rest of this entry »
Posted by David Aspinall 