Course pages 2013–14
Subsections
Hoare Logic
Lecturer: Professor M.J.C. Gordon
No. of lectures: 8
Suggested hours of supervisions: 2
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 and metatheory.
Mathematical interpretation of Hoare logic. Deep and shallow semantic
embedding. Soundness, completeness and decidability.
- Mechanising program verification.
Assertions, annotation and verification conditions. Weakest
preconditions and strongest postconditions; their relationship to
Hoare logic and its mechanisation.
- Additional topics.
Discussion of correct-by-construction methods versus post-hoc
verification. Proof of correctness versus property checking. Recent
developments in Hoare logic such as separation logic.
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.).