Module 08144 (2012)
Syllabus page 2012/2013
The Module Description is a strict subset of this Syllabus Page. (The University module description has not yet been checked against the School's.)
Changes and updates
This module is not offered in 2012/2013
The purpose of this module is to present the basic ideas of program models and modelling; to show how a formal specification of a software component can be written in an appropriate specification language; to present associated techniques, such as the formal refinement of a specification to an imperative program code and the informal implementation of a specification combined with formal proof that the specification is met by the implementation; and to show how to animate a specification in a functional or logical language. It also introduces the ideas and techniques of reasoning about a specification on its own.
The aims of this module are to:
- present the basic ideas and some of the methods of mathematical modelling
- show how a formal specification of a software component can be written
- show how to refine a specification
- show how to implement a specification in an imperative programming language
- show how to animate a specification in a functional programming language
- show how to reason about specifications
|On successful completion of this module, the student should be able to:||Assessed by:|
|1||write a formal specification of a software component in an appropriate language||Examination, Continuous Assessment|
|2||reason about formal specifications and manipulate them, proving the correctness of any transformation||Examination, Continuous Assessment|
|3||carry out simple proofs involving programs and specifications||Examination, Continuous Assessment|
|4||implement a formal specification and prove that the implementation is correct||Examination, Continuous Assessment|
|5||animate a formal specification||Examination, Continuous Assessment|
May not be taken by anyone who has taken or is taking 06-15269 (Formal Methods (Extended)).
2 hr lectures per week
In addition the lecturer is available in office hours and by e-mail.
- Sessional: 1.5 hr examination (80%), continuous assessment (20%)
- Supplementary (where allowed): By examination only.
Last updated: 1 Dec 2008
Source file: /internal/modules/COMSCI/2012/xml/08144.xml