Computer Laboratory

Course pages 2011–12

Hoare Logic

Principal lecturer: Prof Mike Gordon
Taken by: Part II
Past exam questions: Hoare Logic, Specification and Verification I
Information for supervisors (contact lecturer for access permission)

No. of lectures: 12
Prerequisite courses: Logic and Proof

Aims

The aim of the course is to introduce Hoare logic as a basis for the formal specification and verification of imperative programs. A simple language will be used to illustrate core ideas. Both theoretical foundations and the design of mechanized program verifiers will be covered. Some current research activities and challenges will be outlined.

Lectures

  • 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.

  • Additional constructs. Arrays and FOR-commands.

  • Semantics. Mathematical interpretation of Hoare logic. Deep and shallow semantic embedding.

  • Metatheory. Soundness, completeness and decidability.

  • Mechanising program verification. Assertions, annotation and verification conditions. Property checking versus proof of correctness. Interactive versus automatic methods.

  • Predicate transformers. Weakest preconditions and strongest postconditions; their relationship to Hoare logic and its mechanisation.

  • Program refinement. Transforming specifications to programs using refinement rules. Discussion of correct-by-construction methods versus post-hoc verification.

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

  • Review and conclusions. Review of course material covered. Worked examples. Miscellaneous advice on answering examination questions.

Objectives

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 some of 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.).