Reasoning about Programs

Lecturer s : Mark Wheelhouse (homepage) , Sophia Drossopoulou (homepage)
For course notes click on the lecturers homepages.

Aims:

(i) To gain familiarity with use of pre and post conditions and loop invariants for showing correctness.

(ii) To learn some standard algorithms and be able to reason about their correctness.

(iii) To understand the principle of induction and apply it to reasoning about Haskell programs.



Learning Outcomes On completion, a student will

- be able to use mathematical, structural and well-founded induction

- be able to use structural induction when reasoning about Haskell functions.

- be able to reason with pre and post conditions and to use the method of loop invariants to show correctness of programs;

- be familiar with, and understand the development of, some common algorithms, including binary chop, partition and quicksort, Warshall's algorithm and variations, string searching and to reason about them.

Syllabus:

To introduce rigorous reasoning in the specification and design of programs.

Induction: mathematical induction, structural induction, well-founded induction and their relation

Formal program techniques: specification by pre- and post-conditions, derivation and verification of programs, invariants, proofs of program properties. Conversion of recursion to iteration.

Common algorithms as examples (e.g. binary chop, Warshall's algorithm , partition and quicksort, string searching)

Prerequisites: None

Corequisites: Required Course