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