This module addresses the role of formal methods in the software development process, taking an abstract specification and moving towards an executable implementation of that specification.
The module deals with the problems that formal methods are aimed at overcoming, and how they are applied.
Starting with a statement of requirements expressed in English, the approach develops a formal, unambiguous specification of what the software should do. This is then refined through a series of transformations to give executable code faithful to the initial formal specification.
The vocabulary of typed set theory with predicate logic is introduced and a facility in forming set expressions and asserting propositions developed.
A layered approach to design and implementation is explored and its implications for formal development are discussed.
Students gain practical experience in using a state-of-the-art industrial strength formal development support environment during the module.
On successful completion of this module, the student will be able to
Student achievement will be measured by an In-Course Assessment, in which the student will be asked to demonstrate an understanding of the specification and refinement process and skill in the use of an appropriate software validation tool.
Computing Mathematics is a pre-requisite for this module.