[comp.specification] FUZZ

jordan@unix.cis.pitt.edu (Kenneth D Jordan) (02/07/91)

I have heard of a package by Mike Spivey named FUZZ which provides
support for the Z specification language, and I have several questions
which can hopefully be answered by someone with FUZZ experiece.

1.  I understand it's available for a nominal fee.  Any idea of what
    that may be?

2.  Exactly what does it do?  Correctness checking of Z specifications?
    Manipulation of Z (schema renaming, etc.)?  Logical proofs?  Other?

3.  For what platforms is it available?  Is it available in source form?

4.  How generally useful is it; i.e., is it still primarily a research
    tool for the study of Z, or does it have utility for practical
    specifications?

Obviously Mike Spivey's e-mail address would also be helpful.  Thanks
in advance.

--------------------------------------------------------------------------------
                                 Nick Nystrom
                           University of Pittsburgh
                              nystrom@a.psc.edu
--------------------------------------------------------------------------------

bowen@prg.ox.ac.uk (Jonathan Bowen) (02/08/91)

In article <88713@unix.cis.pitt.edu> jordan@unix.cis.pitt.edu
(Kenneth D Jordan) writes:

>I have heard of a package by Mike Spivey named FUZZ which provides
>support for the Z specification language, and I have several questions
>which can hopefully be answered by someone with FUZZ experiece.
>
>1.  I understand it's available for a nominal fee.  Any idea of what
>    that may be?

Between 250 and 300 pounds (1 pound is approx. $2) depending on
the platform and distribution medium.

>2.  Exactly what does it do?  Correctness checking of Z specifications?
>    Manipulation of Z (schema renaming, etc.)?  Logical proofs?  Other?

It type-checks Z documents written using the LaTeX document preparation
system.

>3.  For what platforms is it available?  Is it available in source form?

It currently runs on SUN 3s, SUN 4s (SPARCstations) and IBM PCs.
It is written in C but the source is not available.
It could be ported to other platforms if there was enough demand.

>4.  How generally useful is it; i.e., is it still primarily a research
>    tool for the study of Z, or does it have utility for practical
>    specifications?

I can recommend it. (I am not an employee of Mike Spivey, etc., etc.)
I have used it for all Z documents I have produced in the last year or
two. It is very useful for catching typos but still lets you write
silly and incorrect (although correctly type-checked) specifications.
It is certainly a practical and robust tool if you are happy to
use LaTeX.

>Obviously Mike Spivey's e-mail address would also be helpful.

If you would like an order form, please send a message containing
the command "send z fuzz" to <archive-server@prg.oxford.ac.uk>.
A free LaTeX style option and guide are also available. Send the
command "send z zed.sty zguide.tex" to the same address. However
you don't get the type-checker and nice fonts for the fancy
mathematical symbols with this version.

--
Jonathan Bowen, <Jonathan.Bowen@prg.oxford.ac.uk>
Oxford University Computing Laboratory.