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

Reply via email to