Next:
Tutorial H
Up:
ZUM'95 Tutorials: 4-6th September 1995
Previous:
Tutorial F
TUESDAY 5th September 1995 (afternoon)
A Tutorial on Proof in Standard Z
Stephen Brien, Andrew Martin (Oxford University, UK)
This is a tutorial for users of Z who want to prove properties of their specifications, demonstrate their consistency, or calculate operation preconditions formally. We will show how the deductive system in the Z Standard can be used for these tasks, and discuss the use of specialized derived rules for particular applications. The tutorial will demonstrate use of a simple proof tool being developed in Oxford to support the deductive system from the Standard; it will be available shortly after the meeting.
Stephen Brien has written much of the formal text of the Z Standard, and Andrew Martin is writing the proof tool mentioned above.
See on-line tutorial notes.