2. Week 02: Hoare-Style Poofs and Loop Invariants

2.1. Mandatory Reading

• Variables and loops: Hoare logic (by Xavier Leroy)

2.2. Accompanying Code

• Formalisation of Hoare logic in Coq

2.3. Recommended Reading

• C.A.R. Hoare: An Axiomatic Basis for Computer Programming, 1969
• Edsger W. Dijkstra: Nondeterminacy and Formal Derivation of Programs, 1975
• Stephen A. Cook: Soundness and completeness of an axiom system for program verification, 1978
• Software Foundations (Exercise Book): Hoare Logic