Lecturer	Christie Marr
Degrees	MSc by Research

Overview

 This one-week course will take place in week 9 (16th March 2009).

This course shows how mathematics can be used to structure and reason about information systems. It shows how the Z notation can be used to describe complex pieces of software in a clear and comprehensible fashion. It shows how to check a set of requirements for logical consistency, how to verify that operations are properly defined, and how to ensure that an implementation conforms to its specification by using the techniques of simulations.

Learning outcomes

At the end of the course, students will be able to construct mathematical specifications of real systems. They will be able to check a set of requirements for consistency, reason about the robustness of a design, and confirm that one design refines another.

Prerequisites

Those of you considering taking this course should be aware that before the course commences you must go through Chapters 1-10 of Using Z (you should already know this material, but it's good revision), and also read more thoroughly Chapters 11-18. This reading is a pre-requisite to taking the course.

The course assumes a working knowledge of discrete mathematics. Introduction to Specification is ideal preparation.

Synopsis

• Schema operators: combination; abstract data types; hiding; composition.
• Promotion: structuring specifications; compositionality; replicated structures.
• Preconditions: consistency; applicability; calculation; simplification.
• Case studies: a file system; a bounded buffer.
• Data refinement and simulation.

Reading list

The main course text is:

• J C P Woodcock and J Davies, Using Z, Prentice-Hall, 1996.

The following may also be useful for the Z notation:

• J M Spivey, The Z notation: a reference manual, 2nd edition, Prentice-Hall, 1992.

Taking our courses

This form is not to be used by students studying for a degree in the Department of Computer Science, or for Visiting Students who are registered for Computer Science courses

Other matriculated University of Oxford students who are interested in taking this, or other, courses in the Department of Computer Science, must complete this online form by 17.00 on Friday of 0th week of term in which the course is taught. Late requests, and requests sent by email, will not be considered. All requests must be approved by the relevant Computer Science departmental committee and can only be submitted using this form.