MC144 REASONING ABOUT PROGRAMS (Term 2)

Dr K. Broda and Prof. Sophia Drossopoulou

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 mathematical induction and apply it to reasoning about Haskell programs.

Learning Outcomes

On completion, a student will

- be able to use mathematical induction and structural induction to show that Haskell programs meet their specification;

- 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 (including Boyer Moore algorithm) and to reason about them.

Syllabus:

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

Induction: mathematical induction, structural induction.

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 C140, C120.
Required for C240 Algorithms and Complexity C220 Software Engineering I, C302 Software Engineering - Methods.