Program Construction I (COMP30060)

This module is intended to introduce students to the idea of the formal correctness of algorithms. It begins with a number of lectures and tutorials which show how to prove theorems in the predicate calculus. It next shows 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.