On Tuesday 19 Oct 2010 23:13, Igorj V wrote:
> this document is usefull
> usr011.pdf      ProofPower Z Tutorial
> because i am trying to strugle with Z specification
> language opening excercises

Note that in usr011.pdf it says:

(section 0.5 - Prerequisites)
"We assume a working knowledge of ....
Use of ProofPower as used for specification and proof in HOL"

You may be OK going straight to proof in Z, but the Z 
tutorials are not written with that in mind, and assume that 
you have already done the HOL tutorials.

(section 0.6 - How to use this tutorial)

"you will find some of the material [in usr023.doc] will be 
rejected because definitions have already been made in this 
database. Alternatively you can work from a clean database 
(but then you may find problems if you miss out any of the

The database "example_zed" is the result of running the 
script usr023.doc.  It is suitable for doing the exercises 
but if you try to reload the whole of usr023_slides.doc then 
you will get many failures because of actions which have 
already been done.  To do the exercises in usr011 you should 
work from the file usr011X.doc, and produce something like 
usr011S.doc (which is a set of solutions to the exercises).

If you want to run through usr023_slides.doc, then do it 
using the database "zed".

xpp -f $PPHOME/doc/usr023_slides.doc -d example_zed

Roger Jones
Proofpower mailing list

Reply via email to