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$