Rob, 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. Thanks, Jon On Sun, Aug 26, 2012 at 6:53 AM, Anthony Hall <[email protected]>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: [email protected] > [mailto:[email protected]] 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 > [email protected] > http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com > >
_______________________________________________ Proofpower mailing list [email protected] http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
