Formal Program Design I

For MSc Students Only
Formal Program Design should be taken only by reasonably experienced programmers who wish to learn about formal program proofs.

Overview

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