

CA648  Formal Programming
Module Aims
The module aims to enable students to use mathematical notations
and techniques to enhance significantly the quality of the code
they produce. They will acquire theoretical insight into the mathematics
of specifying and verifying programs.
Learning Outcomes
On successful completion of the module, students should:
 Appreciate the roles of specification, design and coding in
the total task of creating and maintaining good software.
 Understand how mathematical notation can contribute to specifying
computational problems, and have acquired basic skills in one
such formal notation.
 Know how to program with precision from specifications, and
to justify the correctness of programs.
 Be able to use formal mathematics, including logic, to prove
the correctness of programs.
 Be aware of software tools for supporting the creation of quality
code.
Indicative Syllabus
 The language of formal logic; sets, sequences, functions, relations etc.
 Floyd/Hoare logic
 Formal specification
 Partial correctness
 Total correctness
 Program verification
 Program refinement
 EventB
 Tools for supporting EventB e.g. Rodin
Assessment
Continuous assessment: 25 % Endofyear exam: 75 %
Recommended Reading
There is no recommended textbook for this course;
all the necessary reading material will be made available
on the course web page as required.
Supplementary Reading
Modeling in EventB, JeanRaymond Abrial, Cambridge University Press, ISBN 9780521895569
Program Construction: Calculating Implementations from Specifications, Roland Backhouse, Wiley, ISBN 9780470848821
Programming From Specifications, Carroll Morgan
