Module 08144 (2012)
Syllabus page 2012/2013
06-08144
Formal Methods
Level 3/H
Links | Outline | Aims | Outcomes | Prerequisites | Teaching | Assessment | Books | Detailed Syllabus
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
Relevant Links
Outline
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.
Aims
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
Learning Outcomes
| 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 |
Restrictions, Prerequisites and Corequisites
Restrictions:
May not be taken by anyone who has taken or is taking 06-15269 (Formal Methods (Extended)).
Prerequisites:
None
Co-requisites:
None
Teaching
Teaching Methods:
2 hr lectures per week
In addition the lecturer is available in office hours and by e-mail.
Contact Hours:
Assessment
- Sessional: 1.5 hr examination (80%), continuous assessment (20%)
- Supplementary (where allowed): By examination only.
Recommended Books
| Title | Author(s) | Publisher, Date |
| T | T | T, T |
Detailed Syllabus
Not applicable
Last updated: 1 Dec 2008
Source file: /internal/modules/COMSCI/2012/xml/08144.xml
Links | Outline | Aims | Outcomes | Prerequisites | Teaching | Assessment | Books | Detailed Syllabus