Formal Program Design II

Overview

This course deals with specification and data refinement. It shows how modules and systems can be specified abstractly, how algorithms can be developed using abstract datatypes, and how such abstract datatypes can be implemented using concrete datatypes, and that implementation formally justified.

Learning Outcomes

At the end of the course students are expected to:

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