Accessibility statement

Data-Oriented Specifications & their Analysis - COM00023H

« Back to module search

  • Department: Computer Science
  • Module co-ordinator: Dr. Jeremy Jacob
  • Credit value: 10 credits
  • Credit level: H
  • Academic year of delivery: 2019-20

Module summary

Module covers mathematical modelling of data-rich systems and how models relate to designs, and eventually, code.

Professional requirements


Module will run

Occurrence Teaching cycle
A Autumn Term 2019-20

Module aims

Software should do what you expect as reliably as any other technology. Alas, too often it does not. Software is often unreliable and fails to meet the requirements. Typical software defect rates are unacceptable for any other kind of product. This module covers the mathematical modelling, validation, design, and verification techniques that contemporary engineers can employ to save money and time, and reduce risks.

The module concentrates on data-rich systems. A successor module will cover interaction-rich systems.

Module learning outcomes

  • Read and write mathematical descriptions of specifications and designs of data-rich systems;
  • Focus on the pre-condition/post-condition style of specification, but also express a trace-style of specification;
  • Read, write and prove designs as formal refinements of specifications.

Module content

In 2018-19 the module will be taught using the medium of the Z notation, and the tool CZT. Topics covered:

  • The building blocks of the Z notation
  • Use of basic mathematical data structures (sets, relations, functions, bags, sequences)
  • Structuring specifications using the Z notation
  • Refinement: proving that designs respect specifications.

The natural successor module is "Concurrent System Analysis & Verification", which extends the ideas to include interaction-rich systems.


Task Length % of module mark
24 hour open exam
Data-Oriented Specifications & their Analysis (DOSA)
2 hours 100

Special assessment rules


Additional assessment information

The two submitted formative exercises are related to core examinable skills.


Task Length % of module mark
24 hour open exam
Data-Oriented Specifications & their Analysis (DOSA)
2 hours 100

Module feedback

Two practical exercises during the term will be submittable for marking and comment.

Feedback will be available for all practical work during laboratory hours.

Indicative reading

Woodcock J.C.P. and Davies J., Using Z: specification, refinement and proof, Prentice-Hall International, 1996

The information on this page is indicative of the module that is currently on offer. The University is constantly exploring ways to enhance and improve its degree programmes and therefore reserves the right to make variations to the content and method of delivery of modules, and to discontinue modules, if such action is reasonably considered to be necessary by the University. Where appropriate, the University will notify and consult with affected students in advance about any changes that are required in line with the University's policy on the Approval of Modifications to Existing Taught Programmes of Study.

Coronavirus (COVID-19): changes to courses

The 2020/21 academic year will start in September. We aim to deliver as much face-to-face teaching as we can, supported by high quality online alternatives where we must.

Find details of the measures we're planning to protect our community.

Course changes for new students