Learning Module 9 — Hoare Logic

Why this is important: Sometimes you want to be able to demonstrate that a program does what you wanted it to do, i.e., that it’s correct. Hoare Semantics is one way to do this.

Outcomes

• 9.1 – Given two logic expressions, determine which is weaker and which is stronger. (2 point)
• 9.2 – Given a post-condition and an expression, derive the corresponding precondition. (4 points)
• 9.3 – Given a loop, derive a loop invariant and a post-condition. (4 points)