Skip to main content
Logo image

Section C.25 V1: Hoare Logics


  • Recap of correctness definition Section 7.1
  • Correctness up to now was defined on the semantics, on executions of the program.
  • We now develop a logic to reason about correctness without reasoning about executions.
  • Note that the rules of the logic have to be proven correct but that is out of scope.
  • Introduce basic rules of abort and assignment and informally reason about correctness.
  • Block and sequence rules show how free assertions are determined by other rules (assignment).
  • If-then-else example shows that sometimes assertions don't “add up”.
  • Introduce rule of consequence to strengthen preconditions and weaken postconditions.
  • Note that non-matching assertions can be dealt with by the consequence rule which spins off verification conditions

Sections Covered.