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
