next up previous
Next: MC306 Programming Concurrent Computer Up: Year 3 Previous: Year 3

MC301 Formal Software Specifications


MC301 Formal Software Specifications

Credits: 20 Convenor: Gavin Lowe Semester: 1


Prerequisites: essential: MC111, MC206 desirable: MC204
Assessment: Coursework: 30% Three hour exam in January: 70%

Lectures: 36 Classes: 12
Tutorials: 12 Private Study: 90
Labs: none Seminars: none
Project: none Other: none
Total: 150

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 seen in MC206. Some of the algorithms derived will previously have been seen in MC204.

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.

Aims

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.

Objectives

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

Transferable Skills

The ability to reason both abstractly and formally.

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, binary trees; design decisions and performance considerations.

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 coursework will consist of 11 weekly worksheets, and a class test.

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


next up previous
Next: MC306 Programming Concurrent Computer Up: Year 3 Previous: Year 3
S. J. Ambler
11/20/1999