** Next:** Types
** Up:** Michaelmas Term 2002: Part
** Previous:** Project Briefing II
** Contents**

##

Specification and Verification I

*Lecturer: Professor M.J.C. Gordon*
(`mjcg@cl.cam.ac.uk`)

*No. of lectures:* 12

*Prerequisite course: Logic and Proof*

*This course is a prerequisite for Specification and Verification II.*

**Aims**

The aim of the course is to motivate and illustrate the use of
rigorous methods and mechanised tools for reasoning about the
functional behaviour of imperative programs. A goal is to show the
similarities and differences between hardware and software
verification.

**Lectures**

**Program specification.**
Partial and total correctness. Hoare notation. [2 lectures]

**Program verification.**
Axioms and rules of Floyd-Hoare logic. Discussion of soundness and
completeness. [4 lectures]

**Mechanised program verification.**
Annotation. Verification condition generation. [3 lectures]

**Program refinement.**
Definition of the refinement relation. Derivation of laws. [1 lecture]

**Semantic embedding.**
Deep *versus* shallow embedding. Shallow embedding of Hoare
notation in higher order logic. Programming logic as a special case of
general logic. [2 lectures]

**Objectives**

By the end of the course students should have an understanding of some
aspects of the following topics. Partial and total correctness. Hoare
notation. Axioms and rules of Floyd-Hoare logic. Soundness and
completeness. Mechanised program verification using verification
conditions. Program refinement. Semantic embedding in higher order
logic. Limitations of program verification.

**Recommended books**

None (comprehensive notes supplied).

** Next:** Types
** Up:** Michaelmas Term 2002: Part
** Previous:** Project Briefing II
** Contents**
*Christine Northeast*

*Wed Sep 4 14:43:05 BST 2002
*