Specification and Verification I

Lecturer: Prof. 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.

Details below are provisional.

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]

Recommended books:

None (comprehensive notes supplied).