Program Reasoning

Module 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.

Module 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)

Teaching methods

 Lectures and Tutorials

Module leaders

Dr Mark Wheelhouse
Professor Sophia Drossopoulou