Department of Computing
The iframe on this page is empty and contains no contentSkip to content
Search
People

Department of Computing

Home » Reasoning about Programs

> # 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

Main campus address:
Imperial College London, South Kensington Campus, London SW7 2AZ, tel: +44 (0)20 7589 5111
Campus maps and information | About this site

© Copyright 2008 Imperial College London