|Credits: 20||Convenor: Yifeng Chen||Semester: 1|
|Prerequisites:||essential: CO1003, CO1011, CO2006||desirable: CO2004|
|Assessment:||Coursework: 30%||Three hour exam in January: 70%|
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.
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.
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.
Usenet, group comp.risks, ..
Author: N. Rahman, tel: +44 (0)116 252 2593
Last updated: 2004-09-29
MCS Web Maintainer
This document has been approved by the Head of Department.
© University of Leicester.