CO7001 Formal Software Specifications

CO7001 Formal Software Specifications

Credits: 20 Convenor: Yifeng Chen Semester: 1

Prerequisites: essential: CO1003, CO1011, CO2006 desirable: CO2004
Assessment: Coursework: 30% Three hour exam in January: 70%
Lectures: 36 Problem Classes: 12
Tutorials: none Private Study: 90
Labs: none Seminars: none
Project: none Other: none
Surgeries: 12 Total: 150

Subject Knowledge


To appreciate the benefits of writing abstract specifications describing the desired behaviours of computer systems. To appreciate the benefits of using formal techniques to develop programs.

Learning Outcomes

At the end of the course the student should be able to:


Class sessions together with course notes, recommended textbook, worksheets, printed solutions, and some additional hand-outs.


Unassessed coursework, assessed coursework, traditional written examination.

Explanation of Pre-requisites

This course uses mathematics to specify and reason about computer programs. The course builds upon the object-oriented specification and design techniques, and the introduction to VDM seen in CO2006. Some of the algorithms derived will previously have been seen in CO2004.

Course Description

This course demonstrates the use of mathematics to formally specify the requirements of a computer system, and then to develop correct code meeting those requirements.

One of the most common causes of errors in computer systems is that the requirements are incorrectly understood. The purpose of a formal specification is to set down concisely and unambiguously what is required. A good specification concentrates on specifying what is required, not how it will be achieved. To this end, states are specified abstractly (for example, using sets and mappings rather than concrete datatypes such as linked lists or arrays), and specifications are written for the required operations, describing how the state should change.

The process of going from a specification to an implementation is known as refinement. There are two forms of refinement: data refinement and program refinement. Data refinement is concerned with the replacement of the high-level abstract datatypes (e.g. sets and mappings) by the implementable data-types found in languages such as Pascal (e.g. linked lists and arrays). Program refinement is the other part of software development: that of turning specifications into algorithms. also showing

will behind to


The need for formalism and abstraction; specifying programs using pre- and post-conditions; sets, sequences and mappings; specifying states abstractly; state invariants; examples.

Program refinement
What is a proof of correctness; annotating programs; proving annotations correct; proof rules for assignment, sequential composition and alternation; iteration, invariants and variants; finding suitable invariants; examples, deriving common algorithms; deriving efficient programs; functions and procedures.

Data refinement
The concept of data refinement; implementing abstract datatypes; the concept of a retrieve relation; transforming operation specifications to a new datatype; adequacy and totality of the representation; examples: stacks, queues, linked lists.

Reading list



M. Woodman & B. Heal, Introduction to VDM, McGraw-Hill, 1993.

C. B. Jones, Software Development using VDM, Prentice-Hall, 1989. Available on the Web from

D. Andrews, A Theory and Practice of Program Development, Springer, 1997.

A. Kaldewaij, Programming: The Derivation of Algorithms, Prentice-Hall, 1990.


D. Andrews & D. Ince, Practical Formal Methods with VDM, McGraw-Hill, 1991.

C. Morgan, Programming from Specifications, Prentice-Hall, 1994. Available on the Web from

C. B. Jones and R. C. F. Shaw, eds, Case Studies in Systematic Software Development, Prentice-Hall, 1990.

J. Dawes, The VDM-SL Reference Guide, Pitman, 1991.

J. Woodcock & J. Davies, Using Z: Specification, Refinement, and Proof, Prentice-Hall, 1996. Available on the Web from

P.G. Neumann, Computer Related Risks, Addison Wesley, 1995.

Usenet, group comp.risks, ..


Study guide, worksheets, lecture rooms, past examination papers.

Module Evaluation

Course questionnaires, course review.

[University Home] [Faculty of Science] [MCS Home] [CS Home] CS Home Page [University Index A-Z] [University Search] [University Help]

Author: N. Rahman, tel: +44 (0)116 252 2593
Last updated: 2004-01-20
MCS Web Maintainer
This document has been approved by the Head of Department.
© University of Leicester.