[The University of Leicester]

Department of Mathematics & Computer Science



Next: CO3007 Communication and Concurrency Up: Year 3 Previous: Year 3

CO3001 Formal Software Specifications

CO3001 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

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.

Learning Outcomes

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

Methods

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

Assessment

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.

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. Usenet, group comp.risks, ..

Resources

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

Module Evaluation

Course questionnaires, course review.

Next: CO3007 Communication and Concurrency Up: Year 3 Previous: Year 3

[University Home] [MCS Home] [University Index A-Z] [University Search] [University Help]

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