I have a question for you about a particular exception I am running into.
So I have gone through all the tutorial documents, and even after all that
I realize I have a long way to go with getting the hang of things, but I am
currently trying to enter in a small example to try and begin performing
some proofs on it and get comfortable before moving on to my much larger
specifications that I need to prove for my dissertation. I have tried
looking for the answer to the exception in the reference manual, but it is
very large and my search inquiries seem to be coming up empty.

The problem I am having is this. I am trying to use the union operator in
my specification. More specifically I am trying to and a individual item to
a set in the predicate of a specification paragraph in z, which is allowed
by the rules of the language. The PP system comes back with expection 62000
of the Z-Parser, saying that the union symbol from the palette is a free
variable and those are not permitted in Z paragraphs. I certainly do not
want it to be a variable either, I want to use it as a set operator.

Do I need to typecast this symbol as something, such as an ML or HOL object
inside the Z paragraph?

Any help would be greatly appreciated.


On Sun, Aug 26, 2012 at 6:53 AM, Anthony Hall <>wrote:

> Dear All
> I've just got back from holiday (yes, thank you :-) ) and have been reading
> the discussion of ProofPower/Z Word Tools with interest.
> As Rob said, we have been discussing whether and how to integrate the two
> tools, and we did agree that a first step was to make PP work with Unicode.
> ZWT emits Unicode when set to typecheck with CZT, and yes it does allow
> things like Greek characters in names.
> We then discussed two levels of integration.
> The simplest would be a sort of batch integration, similar to the way that
> ZWT works with fuzz or CZT: it would simply hand the whole Unicode file
> over
> to PP to analyse using some sort of potted instruction. This would
> undoubtedly be the simplest way to get started, but is not really how PP is
> meant to work.
> Much better would be a tighter integration where ZWT was able to
> interactively pass selected parts of the spec to PP and return the results
> to Word. This is technically possible but quite a lot of work to do.
> Essentially this would mean that the Word document would be the master
> specification + proof and ZWT would be the UI to PP.
> Whichever way we do this there remains the question of the different
> dialects of Z accepted by PP, fuzz and CZT. In one sense this may not be
> much of a problem: for example requiring the user to have semicolons at the
> end of each line would not stop a specification going through either
> typechecker (although relying on newlines NOT terminating declarations
> obviously would be problematic). Even if the dialect were inconsistent with
> a typechecker, ZWT itself wouldn't mind as long as the lexis was consistent
> - the only likely problem here is that ZWT doesn't distinguish the
> different
> types of unboxed paragraph eg given sets vs free types. Overall I doubt
> whether this is really a huge issue.
> So, Rob, it sounds as if we ought to resurrect our discussions. What do you
> think?
> Incidentally, there is a stable development version of ZWT that is not yet
> released. Its main relevance is that it supports named theorem paras within
> the Z standard (as interpreted by CZT - the standard is a bit of a mess in
> this area). It also has a tool for converting from Spivey to Standard Z. I
> could release it but am working on a couple of other things as well. One is
> a more robust way of delimiting the Z so it's harder to break the document
> structure (or easier not to break it); the other is the perpetual Red Queen
> race to see if the tools will work with Office 2013 or Office 365 or
> whatever it is called this month.
> Anthony
> -----Original Message-----
> From:
> [] On Behalf Of Rob Arthan
> Sent: 13 August 2012 18:13
> To: Jon Lockhart
> Cc: ProofPower List
> Subject: Re: [ProofPower] Trying to Prove my Zed Specifications
> On 13 Aug 2012, at 12:05, Jon Lockhart wrote:
> > Gentlemen,
> >
> > I apologize I should of been more specific at the tasks that I was trying
> to accomplish and in describing where I am at so far.
> >
> > It seems the first point of business though from what Rob is saying is
> actually getting the specifications into the ProofPower environment, which
> at this point sounds like it needs to be done by hand, but I will explain
> it
> more closely Rob. That way you can tell me if I got a shot of importing
> them
> or if I am going to have to do a hand rewrite.
> >
> > So as you mentioned Rob, I am using Anthony's Z Word Tools for Word and I
> have written all my specifications in there so far. It is a fabulous
> writing
> tool, interfacing so well with Word, and providing all the structure I need
> to write the specifications I am working on. Now, I am not sure if you are
> aware of this, but the latest version of the Z Word Tools no longer
> requires
> an export of the specification to be used with FUZZ or CZT, those checkers
> are built right into the tool now and allow for typechecking of the
> specification as you are writing it, using either checker
> I think you will find that Z Word Tools is actually extracting the Z into a
> file and running Fuzz or CZT for you, so it feels like the typechecker is
> built in. You will find that the menu you use to do the typechecking has an
> item on it to export the Z as a file.
> > Now of course, neither of these checkers run on .doc / .docx format
> files,
> and there are a whole host of other files generated when you save or run a
> check, including a LaTeX file of the specification. I was wondering if you
> thought this LaTeX file would be possible to import into the ProofPower
> system, or does it have to be in a special format of .tex to be of any use?
> I actually thought that the CZT unicode format might be a bit closer to
> what
> my prototype tools for dealing with UTF-8 can cope with. If you only have a
> few pages of Z to start with, then it will probably be quicker just to
> reenter it manually. If you have more it may be worth trying to cobble
> together something semi-automated. We should be able to do something much
> slicker in the slightly longer term.
> >
> > I have attached one of the specifications I was originally using to learn
> Z Word Tools, and it has passed all the typecheckers. This is the LaTeX
> file
> that is generated for the specification.
> >
> Thanks.  This reminds me that one of the bigger problems is that ProofPower
> has different rules for newlines than Spivey and the Standard Z.
> Specifically, ProofPower requires semicolons at the end of declarations and
> to separate "stacked" predicates in the predicate parts of schemas.
> Regards,
> Rob.
> _______________________________________________
> Proofpower mailing list
Proofpower mailing list

Reply via email to