Program Construction I

This module is intended to introduce students to the idea of the formal correctness of algorithms. We show how how to specify programs as Precondition, Postcondition pairs. We show how programs can be calculated from such specifications. We also show how we can generalise from these solutions to abstract problems and their solutions.