Department of Mathematics & Computer Science

MC301 Formal Software Specifications

Explanation of Pre-requisites

Course Description

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.

Aims

Objectives

• write an abstract specification describing the requirements of a computer system;
• develop a correct program from a specification;
• implement an abstract datatype.

Transferable Skills

Syllabus

Specification

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

Essential:

Recommended:

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 ftp://ftp.cs.man.ac.uk/pub/cbj/ssdvdm.ps.gz.

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

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

Background:

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 http://www.comlab.ox.ac.uk/oucl/users/carroll.morgan/PfS.

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 http://www.comlab.ox.ac.uk/igdp/usingz/.

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

[[C] ] Usenet group comp.risks.

Details of Assessment

The written exam will contain six questions, covering the breadth of the course. Candidates can obtain full marks from four good answers.

Author: S. J. Ambler, tel: +44 (0)116 252 3884
Last updated: 2001-09-20
MCS Web Maintainer
This document has been approved by the Head of Department.
© University of Leicester.