- Author
- Not stated
- Published
- Undated
- Kind
- Textbook chapter with exercises, from Software Foundations Volume 2
- Original
- softwarefoundations.cis.upenn.edu/plf-current/Hoare.html
- Subject
- Formal methods and proof
What it is
The page is a chapter of an online course text on programming language foundations. It sets out to give tools for verifying that programs meet specifications. It covers assertions, triples and rules for skip, sequencing, assignment, conditionals and loops.
What it says
- The chapter aims to prove formally that particular Imp programs meet their specifications. It uses Floyd-Hoare logic.
- A Hoare triple says a command that starts meeting P and terminates ends meeting Q.
- The assignment rule works backward from the postcondition. The chapter says many people find this backwards at first.
- The rules of consequence let a proof strengthen preconditions and weaken postconditions.
- The while rule rests on the idea of a command invariant.
- The triples describe partial correctness only. A loop that never terminates satisfies any postcondition.
What evidence it gives
The chapter proves each rule valid in Rocq. It applies the rules to small example programs. It also adds automation tactics so that routine assertion checks run by themselves. Exercises ask readers to prove rules and triples, and to extend the logic.
Interests and limits
Only the prose was read closely; code, proofs and later exercises were skimmed. The chapter treats small examples and a toy language. It gives total correctness only a short mention.