Z notation

Lecturer: Jonathan Bowen

Part of the Formal Methods Part II unit (2/CS/3T - CS503) with Nimal Nissanke.

On-line information relevant to the course is available under:

http://www.cs.reading.ac.uk/cs/people/jpb/teaching/z.html

General information

General topics covered on the course. See also specific topics in the Autumn Term.
Recommended books including the Z book used for the course material.
Information on an alternative Z book, with accompanying slides.
Z Glossary in PostScript format (2 pages) and matching L^ATEX source.
Z notation information from the WWW Virtual Library.

Slides (in PostScript format):

Last updated July 1998 with minor corrections and improved formatting.

The following introduce formal methods and general and Z in particular:

Industrial Use of Formal Methods.
Introduction to Z - part I (mathematical notation).
Introduction to Z - part II (schemas).

The following case studies are available:

A File Storage Service.
A Text Formatting Tool ("pos").

One or more case studies will be covered in the lectures, depending on the time available.

Note: please do not print the above. Lecture notes will be issued during lectures and are, in the main, expanded versions of or the same as the slides. Note that PostScript files can only be viewed on Unix workstations (e.g., Suns) rather than PCs in general, if a suitable viewer is available.

You may use the ZTC Z type-checker and the L^ATEX documentation preparation system available on Sun workstations in the department if you wish.

Exercises (in PostScript format):

Last updated July 1998 with minor changes and improved formatting.

Assessments (Summer and Autumn Terms)

Summer Term

You should undertake all the exercises first and obtain the model answers after they have been inspected at tutorials before the assessment test during the Summer Term.

Note that copies of exercises and the assessment test specification are issued at lectures. Please ask me if you need copies because you have missed them at the lectures.

Tutorials

Tutorial times and locations will be announced during lectures and placed on the noticeboard at the main entrance of the Department of Computer Science. Simeon Veloudis and/or Mark Green will be acting as tutorial and practical assistants.

You should attend at least four tutorials during the Summer Term, one for each exercise. Exercises will be issued at lectures and/or on the shelf at the bottom of the main staircase in the Dept of Computer Science. You may do the exercises before or during the tutorial sessions. Answers will be issued at tutorials. exercise. It is important to attempt the exercises and check you understand the answers. If you do not, please ensure you attend the next tutorial and request help.

Note that there will be no lectures during "Reading Week" (normally week 6 of term).

Important note: Answer sheets will be issued at tutorial sessions to encourage attendance! It is an essential part of the course to attend the tutorials and attempt the exercises. This is one of the more mathematically demanding modules; without practice and feedback you will find the examination tough. You will also find the assessment easier if you have finished the exercises beforehand.

Autumn Term

The assessment is a practical to develop, type-check and partially animate a Z specification. You may choose from:

An extended version of the specification you have started to develop for Exercise 4.
An extended version of the Invoicing case study as covered in the lectures.
An example of your own choosing.

The LaTeX source for a initial version of a Z specification (based on Exercise 4) is available to start you off.

Other courses

Foundations, Software Engineering Mathematics, Specification and Design and other courses from IGDP, Oxford University.

Other information

Formal methods research at RUCS.
General formal methods information from the WWW Virtual Library.