# Hoare Logic

Lecturer: Mike Gordon
Taken by: Part II
Number of lectures:12
Lecture location: Lecture Theatre 2, WGB (provisional)
Lecture times: 11:00 on Mon, Wed & Fri starting Fri Oct 07, 2011
Feedback form

Summary: Program specification: partial and total correctness. Hoare notation. Axioms and rules of Hoare logic. Soundness and completeness. Mechanised program verification: verification conditions, weakest preconditions and strongest postconditions. Pointers, the frame problem and separation logic
(Official syllabus)
Material is examinable if it is presented in lectures!

Exercises and past exam questions

Examples classes:

Examples classes will be run by John Wickerson in Room FW26.

• The first class will be on Tue 25 Oct, 1600-1730.
John writes: in the first examples class we will work through the following exercises. Feel free to have a go at them beforehand if you like.
• 2005 Paper 7 Question 6
• 1993 Paper 10 Question 12. Parts (a)-(c).
• Consider this program, written in a C-like language:
``` x = 1; while (z > 0) {   if (z & 1 == 1) x = y * x;   z = z >> 1;   y = y * y; } ```
Work out what it is supposed to do, invent a sensible specification for it, and prove that the specification holds.

• The second class will be on Wed 09 Nov, 1530-1700. In this we will work through 2006 Paper 8 Question 15 (feel free to have a go beforehand), and then talk about Separation Logic.

Slides

The whole set of slides is available both as a single document:

or split into sections:

The actual slides presented in each lecture: Oct 7, Oct 10, Oct 12, Oct 14, Oct 17, Oct 19, Oct 21, Oct 24, Oct 26, Oct 28, Oct 31, Nov 2 (Holfoot).

• John Wickerson gave a guest lecture on October 21 on VCC.
• VCC can be tried online at rise4fun.com/vcc.
• Alternatively it can be downloaded from vcc.codeplex.com. You will need a working installation of MS Visual Studio 2010. Please note the following three common problems with VCC installation and use:
1. You must make a Visual Studio project before you can begin verifying. In the project properties, select "Configuration properties", then "VC++ directories", and then add \$(INCLUDE) to the end of the list of "Include directories".
2. Any file you verify must be part of a project, otherwise you will get an "Object instance not set to an object" error. If you right-click on the project and select "Add item", then you can be sure that your file is part of the project.
3. In the VCC options (available from the Verify menu), ensure that VCC version is set to "V3". This version uses very different syntax from previous versions of VCC.
• Here is a zip file containing the 6 source files verified during the lecture, plus selection-sort which was left as an exercise.
• John's lecture to the 2010 MPhil/ACS course describes hand proofs of the linked list reversal program first using original 'old style' Hoare logic (which is what VCC implements) and then using separation logic (whose implementation is the subject of current research).