Formal Program Design I

For MSc Students Only
Please note that you cannot take Formal Program Design and Procedural Programming - you may take only one of these options. Formal Program Design should be taken only by reasonably experienced programmers who wish to learn about formal program proofs.

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 aim is to show how procedural programs can be developed rigorously from their mathematical specifications. In the first part, the emphasis is primarily on how to derive loops from invariants; this activity is called algorithm refinement.

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