Course material 2010–11
Hoare Logic
Lecturer: Professor M.J.C. Gordon
No. of lectures: 8
Prerequisite courses: Logic and Proof
Aims
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.
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.
- 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.
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 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.).