Module 08144 (2012)

Module Description - Formal Methods

The Module Description is a strict subset of the Syllabus Page, which gives more information

Module TitleFormal Methods
SchoolComputer Science
Module Code06-08144
DescriptorCOMP/06-08144/LH
Member of StaffUnassigned
LevelH
Credits10
Semester2
Pre-requisites None
Co-requisites None
RestrictionsMay not be taken by anyone who has taken or is taking 06-15269 (Formal Methods (Extended)).
Contact hours 22
Delivery2 hr lectures per week
In addition the lecturer is available in office hours and by e-mail.
Description 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.
Outcomes
On successful completion of this module, the student should be able to:Assessed by:
write a formal specification of a software component in an appropriate language Examination, Continuous Assessment
reason about formal specifications and manipulate them, proving the correctness of any transformation Examination, Continuous Assessment
carry out simple proofs involving programs and specifications Examination, Continuous Assessment
implement a formal specification and prove that the implementation is correct Examination, Continuous Assessment
animate a formal specification Examination, Continuous Assessment
AssessmentSessional: 1.5 hr examination (80%), continuous assessment (20%)
Supplementary (where allowed): By examination only.
TextsTo be provided later.