Computer Laboratory

Course material 2010–11

Hoare Logic

Lecturer: Professor M.J.C. Gordon

No. of lectures: 8

Prerequisite courses: Logic and Proof


The aim of the course is to show how Hoare logic provides a basis for the formal specification and verification of imperative programs. A simple language will be used to illustrate core ideas. Some current research activities and challenges will be outlined.


  • Formal specification of imperative programs. Formal versus informal methods. Specification using preconditions and postconditions.

  • Axioms and rules of inference. Hoare logic for a simple language with assignments, sequences, conditionals and while-loops.

  • Loops and invariants. Various examples illustrating loop invariants and how they can be found.

  • Partial and total correctness. Hoare logic for proving termination. Variants.

  • Semantics. Mathematical interpretation of Hoare logic. Soundness and relative completeness.

  • Mechanising program verification. Weakest preconditions and strongest postconditions. Verification conditions.

  • Automated theorem proving. Property checking versus proof of correctness. Interactive versus automatic methods.

  • Current reseach. Recent developments in Hoare logic such as separation logic.


At the end of the course students should

  • be able to prove simple programs correct by hand and implement a simple program verifier;

  • be familiar with the theory and use of Hoare logic and its mechanisation;

  • understand the core concepts underlying modern formal program verification.

Recommended reading

Huth, M. & Ryan M. (2004). Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press (2nd ed.).