Reasoning about Programs
(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.
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.
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)
Lectures and Tutorials
Module leadersDr Mark Wheelhouse
Professor Sophia Drossopoulou