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 material)." 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 Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
