module specification

CC3007 - Formal Methods of Specification (2017/18)

Module specification Module approved to run in 2017/18, but may be subject to modification
Module title Formal Methods of Specification
Module level Honours (06)
Credit rating for module 15
School School of Computing and Digital Media
Assessment components
Type Weighting Qualifying mark Description
Coursework 60%   Coursework (Electronic Submission to Module Leader)
Unseen Examination 40%   Unseen Exam *FC*
Running in 2017/18 No instances running in the year

Module summary

The module introduces a model based formal specification language that is used to provide the students with knowledge and skills to produce formal specifications from informal descriptions.

Prior learning requirements

Prerequisite: MA1032N Logic or CC2010N Programming and Data Structures or equivalent
Co-requisite: CC3008N Software Architecture

Module aims

The principal graduate attributes focused on in the module are ‘Performance in a variety of idioms and contexts’ [A2] and ‘Creative and Ethical’ [A3].
The module aims to introduce a model based formal specification language [A2] and provide students with the knowledge and skills to construct formal specifications from informal descriptions [A2, A3] as well as refine their specifications for implementation [A3].


- Rationale for the use of formal specification [A2].
- In-depth study of a model based formal specification language (e.g. Z) [A2].:
o Representational and procedural abstraction using sets and logic, relations, functions and sequences.
o The schema calculus.
o The mathematical toolkit.
o Extension of the language via generic axiomatic definition.
- Software tools to support specification development [A2]..
- Development of substantial case studies, individually and in groups [A2, A3]..
· Basics on Object-oriented variation of the formal specification language already introduced (e.g. Object Z) [A2].

Learning and teaching

Students will develop their theoretical understanding from interactive lectures (22 hours). Typically, a new concept will be introduced, then used in developing and discussing many small specification fragments. Such lectures will be concentrated at the beginning of the course. Supervised tutorials (22 hours ) will be used for development of larger specifications, often in groups, which will require the application of more of the taught material. The students will also be required to undertake non-supervised work (106 hours) on individual and group case studies, some of which will be part of the assessment for the module. The implementation of the latter will also be part of the assessment for the co-requisite module CC3008N.

Learning outcomes

On completing the module the student should be able to (the attributes achieved are in brackets):
LO1 - Understand the advantages of using formal specification [A2]
LO2 - Develop formal specifications from informal problem statements [A2, A3].
LO3 - Understand and critically appraise specifications written by others [A2].
LO4 - Refine specifications through different levels of abstraction [A2, A3].
LO5 - Extend the specification language where necessary for an application [A3].

Assessment strategy

This module is assessed through a coursework and an examination.

- The coursework assignment is based on a Case Study, consisting of a formal specification produced on the basis of provided informal descriptions of requirements. This part is conducted in a group in order to encourage communication and to guide the students to undertake solving a problem in a guided group structure. Formative feedback is provided throughout the whole of the duration of the coursework.
This assessment component assesses the Learning Outcomes LO3 ,LO4 and LO5.

- The final examination is a summative assessment and examines the students’ knowledge and understanding of formal specification in general as well as ability to develop formal specifications from informal problem statements and understand the meaning of other formal specifications. This component assesses the students in Learning Outcomes LO1, LO2, LO3 and LO4.


Currie, E
The Essence of Z
Prentice Hall Europe.

Lightfoot, D
Formal Specification using Z

Woodcock, J. and Davies, J.
Using Z
Prentice Hall;