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

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.


-----Original Message-----
[] 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.



Proofpower mailing list

Proofpower mailing list

Reply via email to