CA648 - Formal Programming
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.
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
- The language of formal logic; sets, sequences, functions, relations etc.
- Floyd/Hoare logic
- Formal specification
- Partial correctness
- Total correctness
- Program verification
- Program refinement
- Tools for supporting Event-B e.g. Rodin
Continuous assessment: 25 % End-of-year exam: 75 %
There is no recommended textbook for this course;
all the necessary reading material will be made available
on the course web page as required.
Modeling in Event-B, Jean-Raymond Abrial, Cambridge University Press, ISBN 9780521895569
Program Construction: Calculating Implementations from Specifications, Roland Backhouse, Wiley, ISBN 978-0470848821
Programming From Specifications, Carroll Morgan