Specification and Verification I
Lecturer: Mike Gordon
Taken by: Part II
Number of lectures: 12
Lecture location: Lecture Theatre 2, WGB
Lecture times: 12:00 on Mon, Wed & Thu starting Fri Jan 15, 2010
Summary: Program specification: partial and total correctness.
Hoare notation. Axioms and rules of Hoare logic.
Discussion of soundness and completeness. Mechanised program
verification: verification conditions. Program refinement. Semantic
embedding in higher order logic.
Past exam questions
(warning: old questions may contain material not examinable in the current course)
Material is examinable if it is presented in lectures!
[A3 postscript (for projection) |
A4 pdf |
A4 pdf (4 slides per page)]
(warning: slides for lectures not yet
given might change or be omitted)
Related course: This course is a prerequisite for
Specification and Verification II
Acknowledgement: Some of the teaching materials in this course were
prepared by Dr Paul