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
• Event-B
• Tools for supporting Event-B e.g. Rodin

Assessment

Continuous assessment: 25 % End-of-year 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

Program Construction: Calculating Implementations from Specifications, Roland Backhouse, Wiley, ISBN 978-0470848821

Programming From Specifications, Carroll Morgan