Module 08144 (2008)
Syllabus page 2008/2009
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.)
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/2008/xml/08144.xml
Links | Outline | Aims | Outcomes | Prerequisites | Teaching | Assessment | Books | Detailed Syllabus