Joan.Arnold@prg.oxford.ac.uk (06/03/91)
OXFORD UNIVERSITY COMPUTING LABORATORY
PROGRAMMING RESEARCH GROUP
Advanced Z Course on Proof at Lady Margaret Hall Oxford
from Sunday 21st July --- Friday 26th July, 1991
For further details contact:
Joan Arnold
Programming Research Group
Computing Laboratory
Oxford University
8-11 Keble Road
OXFORD OX1 3QD
Telephone: (0865) 272579
OBJECTIVES
The objective of the course is to provide an introduction to
formal reasoning in Z, and to show how it can be used as part of
the development process. The course describes the newly
defined logic for Z, and shows how it can be used by hand and by
machine to prove properties of Z specifications. The emphasis is on
tutorial exercises and practical work with a simple computer-based
proof tool, so that students can gain confidence in applying formal
reasoning. Students are expected to have some experience of Z.
COURSE OUTLINE
The course takes the form of 7 lectures, 6 tutorials and 6
practical sessions. The lectures have the following outline:
Propositional Calculus:
Introduction to the logic of Z; left-rules and right rules;
anatomy of a rule; applying rules and backwards reasoning; the
propositional calculus and Z; equational reasoning.
Predicate Calculus:
The predicate calculus quantifiers in Z; strategies for
quantifier proofs; a notation for recording proofs.
Set Theory:
Undefined terms; equality and membership; the axioms for set
theory in Z; adding laws to the basic library.
A Schema Calculus:
Rules for introducing and eliminating schemas; the left-rules;
schema equality.
Using B:
Introduction to the B proof assistant; the implementation of
the logic of Z; conducting proofs in B; the rule language;
the tactic language.
Preconditions:
Precondition analysis in Z; equational reasoning under an
hypothesis; zedB.
Structured Proofs:
Coping with large-scale verification; compositionality; some
theorems in the schema calculus.
Timetable
9:00-10:30 11:00-12:30 2:00-3:30 4:00-5:30
------------------------------------------------------------------------
Monday Propositional Tutorial Predicate Tutorial
Calculus Calculus
------------------------------------------------------------------------
Tuesday Set Theory Tutorial A Schema Tutorial
Calculus
------------------------------------------------------------------------
Wed Using B Practical Practical Practical
------------------------------------------------------------------------
Thursday Preconditions Tutorial Structured Tutorial
Proofs
------------------------------------------------------------------------
Friday Practical Practical Practical
------------------------------------------------------------------------
The 4 days of lectures are all divided into four sessions.
On most days there are tutorial sessions, during which the participants
will be asked to tackle exercises covering the material presented.
All lectures will be followed by a discussion period, during which
additional small exercises will be given.
Extra sessions will be arranged if we find additional appropriate
topics to present.
BACKGROUND READING
The level of the teaching will be tailored to suit the needs of the
particular audience. We assume that all participants have a basic
understanding of Z.
By way of preparing for the course we recommend revision from a
suitable text book on Z, for example:
J. Woodcock & M. Loomes, "Software Engineering
Mathematics", Pitman, 1988.
J.M. Spivey, "The Z Notation: A Reference Manual",
Prentice-Hall, 1989.
COURSE MATERIAL
A variety of relevant material will be available during the course
including:
Lecture Notes on Logic and Proof in Z.
Exercises.
Solutions.
Reference manuals.
LECTURERS AND TUTORS
Lecturers: Stephen Brien
Divya Prasad
Jim Woodcock
LOCATION, ACCOMMODATION, MEALS
All lectures and tutorial sessions will be held in Lady Margaret
Hall, Norham Gardens, Oxford.
Coffee will be available during the morning break (10.30 am) and
tea during the afternoon break (3.30 pm). Accommodation is
provided in Lady Margaret Hall, and all rooms are reserved for
the period of the course, i.e. Sunday 21st July to Friday 26th
July at 3.30 pm.
Breakfast will be served from 8.15 to 9.00 am. Lunch will be
served from 1.00 pm to 2.00~pm and dinner will commence at 7.00
pm.
On the Thursday evening there will be a special course dinner.
\section*{Course Facilities}
%
During the course, attendees will have access to College facilities
(e.g. television room, sports facilities, games room and College
bar). Further information will be available on arrival.
ARRIVAL AND DEPARTURE
All participants are expected to arrive in Oxford on Sunday 21st
July from 5:00 pm onwards.
On arrival go to Lady Margaret Hall (a map will be provided),
and obtain your key from the Lodge.
Please note that there is no admittance to the College after
11.00 pm. If you intend to arrive after this time, please
inform us in advance.
A buffet will be provided in the College between 7.00 and 9.00
pm on Sunday 21st. An informal session will be held in the
College bar afterwards.
The week's activities will draw to a close after tea on Friday
26th July, and your room must be vacated before the session
starts at 9.30 on Friday 26th. We will arrange for the storage
of luggage until departure.
COST
Tuition fees 1,000 pounds per person
Meals & Accommodation 275 pounds per person
COURSE ADMINISTRATION
As there are a limited number of places available (16), please send
your registration as soon as possible, (not later than Friday 21st June
1991) to:
Joan Arnold
Programming Research Group
Computing Laboratory
8-11 Keble Road
Oxford
OX1 3QD
Any enquiries about registration or any other problems, which may
arise before or during the course, should be made to:
Joan Arnold
Tel: (0865) 272579
Messages for attendees during the course should be directed to
Lady Margaret Hall. Please contact the Porter's Lodge, tel 0865
274300.
=======================================================================
=======================================================================
OXFORD UNIVERSITY COMPUTING LABORATORY
PROGRAMMING RESEARCH GROUP
REGISTRATION FORM
Z Course in Proof
Sunday 21st -- Friday 26th July 1991
I wish to reserve a place for the course `Z in Proof' to be held
at Lady Margaret Hall, Norham Gardens, Oxford, from Sunday 21st July
to Friday 26th July 1991 at a cost of:
1,000 pounds for tuition fees ..................................(Yes/No)
275 pounds for meals and accommodation
(at Lady Margaret Hall).........................................(Yes/No)
Please state any special dietary requirements ..........................
TITLE:.................................................................
SURNAME:................................................................
FIRST NAME:.............................................................
ORGANISATION:...........................................................
ADDRESS:
........................................................................
........................................................................
Postcode:....................................................
TELEPHONE:...........................FAX:....................
E-MAIL:......................................................
PLEASE SEND INVOICE TO:
.......................................................................
.......................................................................
SIGNED:.............................DATE:..............................
Please photocopy and complete a separate form for each participant and
return (not later than 21st June,1991) to:
Joan Arnold
Programming Research Group
Oxford University Computing Laboratory
8--11 Keble Road
OXFORD OX1 3QD
Tel: (0865) 272579
Fax: (0865) 273839
JANET:joan@uk.ac.oxford.prg