- Author
- Not stated
- Published
- Undated
- Kind
- Textbook chapter with exercises, from Software Foundations Volume 2
- Original
- softwarefoundations.cis.upenn.edu/plf-current/Hoare2.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 make Hoare logic proofs compact and mostly automatic. It ends with an optional section on weakest preconditions.
What it says
- The chapter says Hoare logic is syntax directed. Proof structure follows program structure exactly.
- A decorated program places assertions around each command. The chapter calls it a compact form of a Hoare logic proof.
- Assertions can be derived mechanically by working backward from the postcondition. The chapter says finding loop invariants is the only creative part.
- A loop invariant must hold on entry and imply the postcondition on exit. It must also survive one pass of the loop body.
- A worked example guesses True and then the postcondition as invariants, and both fail. The invariant that the gap between Y and X stays constant succeeds.
- A variable the loop only reads must be recorded as unchanged in the invariant.
- The chapter defines decorated programs formally and builds a generator of verification conditions. It then proves that generator correct.
What evidence it gives
The chapter works through example programs, including swapping, division, subtraction and parity. It proves in Rocq that its verification condition generator is correct. Many exercises ask for decorations and proofs, such as factorial and Fibonacci.
Interests and limits
Only the prose was read closely; code, formal proofs and most exercises were skimmed. The examples are small programs in a toy language. The chapter does not test its methods on real software.