Specification and Verification I

Lecturer: Prof. M.J.C. Gordon (mjcg@cl.cam.ac.uk)

No. of lectures: 12

Prerequisite course: Logic and Proof  

Program specification.

Partial and total correctness. Hoare notation.

Program verification.

Axioms and rules of Floyd-Hoare logic. Discussion of soundness and completeness.

Mechanised program verification.

Annotation. Verification condition generation.

Program refinement.

Definition of the refinement relation. Derivation of laws.

Semantic embedding.

Deep versus shallow embedding. Shallow embedding of Hoare notation in higher order logic. Programming logic as a special case of general logic.

Recommended books:

None (comprehensive notes supplied).