Change “Z” on the first line of your Z paragraph to “ZAX” and all should be 
well. Spivey Z, ProofPower-Z and ISO Z all require this bit of mark-up to 
distinguish axiomatic descriptions with the predicate part omitted (what you 
want) and given set definitions, free type definitions and constraints. The 
typesetting in ProofPower-Z is not quite in line with Spivey Z and ISO Z, 
because it gives you independent control of whether to print the vertical  bar 
on the left, whereas I think the presence or absence of the vertical bar is 
intended to be a visual clue to what kind of paragraph you have in Spivey Z and 



On 19 Jun 2014, at 17:59, Jon Lockhart <> wrote:

> Dear All,
> I am throwing an odd exception recently when working on a small example 
> specification. In checking the manuals and Z books there seems to be no 
> reason that this exception is being thrown. It is even used in the vending 
> machine example in the Z Tutorial book. I have attached the exact piece that 
> is giving me the exception and the output from ProofPower. 
> If anyone has any ideas on what might be causing it, please let me know.
> Regards,
> Jon Lockhart
> PhD Candidate
> EE Systems
> University of Cincinnati
> <simpleError.doc>_______________________________________________
> Proofpower mailing list

Proofpower mailing list

Reply via email to