Formal Program Design II

Overview

This course follows on from the Mods course on procedural programming, though it can also be taken independently with some previous programming experience. The second part of the course deals with data refinement, and shows how efficient data structures can be introduced into a program. Towards the end of the course, the subject of refining specifications of larger systems is broached.

Learning Outcomes

At the end of the course students are expected to:

• Be able to specify modules, and in particular programs, abstractly
• Perform rigorous and even formal derivations of efficient programs from their abstract specifications
• Understand the criteria for algorithm refinement and data refinement