This howto shows how to install the Fuzz typechecker tool for Z specifications on Cygwin. It includes a shell script that performs routine tasks. Z is a math notation used to improve the reliability of software systems.

For info on the Fuzz typechecker for Z, please see
  http://spivey.oriel.ox.ac.uk/~mike/fuzz/

For info on Z, see
  http://archive.comlab.ox.ac.uk/z.html

   Installing Fuzz on Cygwin, a Linux Flavor.
   ==========================================
By Christopher M. Balz.

Last updated November 04, 2004.

This HOWTO tested with Fuzz 2000 on:
               GNU bash, version 2.05b.0(1)-release (i686-pc-cygwin)
               Copyright (C) 2002 Free Software Foundation, Inc.
           with the i686-pc-cygwin running on Windows XP SP2.

Known Issues with this procedure: None.


1) What is Cygwin?

Cygwin is a RedHat, Inc. product.  It is a flavor of
Linux that runs on top of Windows.



2) Why would I want Cygwin?

The main reason is that the best version (which is
also a free version) of Fuzz runs on Unix, of which
Cygwin is a flavor.

Other reasons: Cygwin is a free way to run Linux
without having to dedicate an entire hard drive or
partition of a hard drive to Linux.  It also enables
you to run Linux inside a regular Windows GUI window
without having to run the not-cheap VMWare program.
Running Linux from a regular window on Windows enables
you to instantly access all that Linux has to offer
(with emphasis on technical tools) while on running
Windows.


3) What software do I need to make full use of Fuzz?

LaTex, a text editor such as Emacs, and a PostScript
file displayer such as Ghostview.

Fuzz checks Z specifications for correctness.  LaTex
is required for Fuzz.  Emacs has a venerable built-in
editing mode for Tex and LaTex.  LaTex files can be
easily processed into PostScript files, to see the
final result of the LaTex source code.  LaTex, Emacs,
and Ghostview are available as
automatically-installable packages for Cygwin. Builds
of these programs exist for Windows.  If you use a
Windows editor to create a 'tex' file destined for
Fuzz, you will need to run the utility (built into
Cygwin) 'dos2unix' on it before Fuzz will work on it.


3) Get Cygwin.

Cygwin is available from http://cygwin.com. An
optional, excellent GUI desktop called the KDE,
commonly found on GNU/Linux systems, now runs on
Cygwin!  It is available as a build for Cygwin from
the KDE Project (kde.org).  The KDE works pretty well
on Cygwin and is not too hard to install.


4) Get Fuzz from the downloads section of J. M.
Spivey's Fuzz page.


5) Save the fuzz2000 directory in '/usr/share/'.


6) Make Fuzz an executable program from anywhere on
Cygwin:

        ln -s c:/cygwin/usr/share/fuzz2000/src/fuzz.exe
fuzz.exe


7) Change all instances of "Syntax" in the file
'test2.exp' (located in the 'test' directory of the
Fuzz download) to "syntax".



8) Read the file named 'INSTALL', but do not do
anything else yet.



9) Ensure the existance of the directory (create only
if it does not exist):

       /usr/local/lib/


10) Ensure the existance of the directory (create only
if it does not exist):

      /usr/share/texmf/fonts/source/local


11) Change the following lines in the Makefile

      TEXDIR = /usr/lib/tex/texmf/tex
      MFDIR = /usr/lib/tex/texmf/fonts/source/local

      so that they look like this:

      # TEXDIR = /usr/lib/tex/texmf/tex
      # MFDIR = /usr/lib/tex/texmf/fonts/source/local


12) Add the following two lines directly below them:

     TEXDIR = /usr/lib/texmf/tex
     MFDIR = /usr/share/texmf/fonts/source/local


13) Ensure that your texhash command will be
permitted, enter the following command at the Cygwin
command prompt:

        chmod 777 /usr/share/texmf/ls-R


14) Follow the directions in the INSTALL file, noting
that:
       * Save the output of the commands given in the
INSTALL file in case you need them for debugging
later.
       * Nothing needs to be done for Step 1 in the
INSTALL file.
       * the 'su -c' in 'su -c "make install"' will
probably not be needed on your particular Cygwin
installation, because Cygwin installs with no 'root'
user.



15) Restore the default system permissions that were
altered in Step 9 by entering the following command at
the command prompt:

        chmod 775 /usr/share/texmf/ls-R


16) Copy and save the shell script below (starting with '#!/usr/bin/bash')
to a file named 'fuzzify.sh' (without the single quotes).  Do this
starting, inclusively, with '#!/usr/bin/bash' and ending with 'exit
0'.  Make sure that any line breaks picked up from your copy-paste
operation do not break the shell's syntax rules.  If any do,just delete the
problem line breaks.  Read the instructions for installing and operating
the shell script in the comments at the head of the shell script.  Follow
these instructions.

#!/usr/bin/bash
# 'fuzzify.sh'
# Version: 1.1
#
# Author: Christopher M. Balz
# September 12, 2004
# Last updated: November 04, 2004.
#
# What is this?
#    This is a simple utility to make it easy and fast to develop
#    LaTex files for the Fuzz Z Specification checker.
#
# What does this utility do?
#    It runs 'LaTex' on a given 'tex' file,
#    then runs 'fuzz' on the file, then runs 'dvipdf' on the dvi file, and
then
#    displays the file in a PostScript file viewer.
#
# Testing: Tested on command-line Cygwin on Windows XP with the Windows
build of
#          the Adobe Acrobat (tm) PDF file viewer program, and with the
#          'GSview' PostScript file viewer program.
#
# Installation: Create a file with these contents in '/usr/share/'.
#               Then issue the command,
#                 'ln -s /usr/share/fuzzify.sh /usr/sbin/fuzzify'
#
# Operation: To run: First close any existing PDF viewer program window
#            (this may or may not be
#            necessary, depending on the build of the PDF file viewer
#            program that you are using).
#            Next, enter the command,
#              'fuzzify <your file name without the filename extension>'
#            (For example, say 'fuzzify example' to fuzzify 'example.tex').
#
#            * Note:  If 'LaTex' does not like your file, the problem may
be DOS
#                     end-of-line characters.
#                     Try running 'fuzzify' with this command:
#
#                      'fuzzify <your file name without the filename
extension>' -d
#
#                     and 'fuzzify' will first process the file with
'dos2unix',
#                     a standard and venerable Unix-flavored program.
#
# Modification: To make this program use the PostScript file format, simply
#               uncomment-out and comment-out the relevant lines below.

if [ -z $2 ]
     then
     echo
else
     if [ $2 = "-d" ]
         then
         echo;echo Running dos2unix on $1.tex . . .
         dos2unix $1.tex
         echo
     fi
fi

echo Fuzzify will now latex your file $1.tex . . .
echo;

tex=$1.tex
dvi=$1.dvi
ps=$1.ps
pdf=$1.pdf

latex $tex

echo;
echo Fuzzify will now run fuzz on $tex . . .
echo

fuzz $tex


# echo;
# echo Fuzzify will now turn $tex
# into a PostScript file and display it using \'gsview32.exe\' . . .
# echo
# dvips $dvi
# c:/Windows/System32/cmd.exe /c "C:\Program
Files\Ghostgum\gsview\gsview32.exe" $ps &


echo;
echo Fuzzify will now turn \'$tex\' into a PDF file and display it using
\'AcroRd32.exe\'.
echo         $'\t' \* Note that with some PDF viewers, the PDF file viewer
program must be closed
echo         $'\t' $'\040' before this command runs in order for this
command to run successfully.
echo;

dvipdf $dvi;
c:/Windows/System32/cmd.exe /c "c:\Program Files\Adobe\Acrobat
6.0\Reader\AcroRd32.exe" $pdf &

echo;echo Fuzzify will now exit.
echo;

exit 0



17) Check your make results against the following to
ensure that the installation worked correctly (the
'bash-2.05b$' text below is just the Unix shell
command prompt identifier).

bash-2.05b$ cd fuzzlib
bash-2.05b$ make
make -C src all
make[1]: Entering directory
`/usr/local/lib/fuzzlib/src'
bison -dv -y zparse.y
conflicts: 5 shift/reduce
mv y.tab.h symbol.h
mv y.tab.c zparse.c
gawk -f absyn.k absyn.x >absyn.h
gcc  -c -DDEBUG -DANSI -DASSUME zparse.c
flex -s -t zscan.l > zscan.c
gcc  -c -DDEBUG -DANSI -DASSUME zscan.c
gcc  -c -DDEBUG -DANSI -DASSUME param.c
gcc  -c -DDEBUG -DANSI -DASSUME main.c
gcc  -c -DDEBUG -DANSI -DASSUME spec.c
gcc  -c -DDEBUG -DANSI -DASSUME type.c
gcc  -c -DDEBUG -DANSI -DASSUME frame.c
gcc  -c -DDEBUG -DANSI -DASSUME dict.c
gcc  -c -DDEBUG -DANSI -DASSUME sched.c
gcc  -c -DDEBUG -DANSI -DASSUME pretty.c
gcc  -c -DDEBUG -DANSI -DASSUME error.c
gcc  -c -DDEBUG -DANSI -DASSUME expr.c
gcc  -c -DDEBUG -DANSI -DASSUME alloc.c
gcc  -c -DDEBUG -DANSI -DASSUME unify.c
gcc  -c -DDEBUG -DANSI -DASSUME schema.c
gcc  -c -DDEBUG -DANSI -DASSUME dump.c
gcc  -o fuzz zparse.o zscan.o param.o main.o spec.o
type.o frame.o dict.o sched.o pretty.o error.o expr.o
alloc.o unify.o schema.o dump.o
/lib/cpp -DDEBUG -DANSI -DASSUME symdef.x >symdef.i
gawk -f fuzzlib.k output=fuzzlib fuzzlib.x >fuzzlib
gawk -f fuzzlib.k output=minilib minilib.x >minilib
rm symdef.i
rm zscan.c
make[1]: Leaving directory
`/usr/local/lib/fuzzlib/src'
bash-2.05b$ make test
make -C test test
make[1]: Entering directory
`/usr/local/lib/fuzzlib/test'
../src/fuzz -p ../src/fuzzlib -t -d test1.in 2>&1 |
diff test1.exp -
../src/fuzz -p ../src/fuzzlib -t -d test2.in 2>&1 |
diff test2.exp -
../src/fuzz -p ../src/fuzzlib -v test3.in 2>&1 | diff
test3.exp -
../src/fuzz -p ../src/fuzzlib -t -d test4.in 2>&1 |
diff test4.exp -
../src/fuzz -p ../src/fuzzlib -t -d test5.in 2>&1 |
diff test5.exp -
../src/fuzz -p ../src/minilib -t -d test6.in 2>&1 |
diff test6.exp -
../src/fuzz -p ../src/fuzzlib -t -d test7.in 2>&1 |
diff test7.exp -
../src/fuzz -p ../src/fuzzlib -t -d test8.in 2>&1 |
diff test8.exp -
make[1]: Leaving directory
`/usr/local/lib/fuzzlib/test'
bash-2.05b$

bash-2.05b$ make install
make -C src all
make[1]: Entering directory `/usr/share/fuzz2000/src'
make[1]: Nothing to be done for `all'.
make[1]: Leaving directory `/usr/share/fuzz2000/src'
install -m 755 src/fuzz /usr/local/bin
install -m 644 src/fuzzlib /usr/local/lib
install -m 644 tex/fuzz.sty /usr/lib/texmf/tex
install -m 644 tex/*.mf
/usr/share/texmf/fonts/source/localn
bash-2.05b$