Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456 Hoare Logic (CST Part II)
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!
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.
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.
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:
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".
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.
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).
Separation logic inspired startup Monoidics and their tool
INFER.
Starting from about 28:26 minutes
into this
video there is a nice introduction to metamathematics (soundness,
completeness, Goedel's theorem, Turing machines etc.).