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: proofpower-boun...@lemma-one.com [mailto:proofpower-boun...@lemma-one.com] 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@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com _______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
