CMU MSE 15-671 Models of Software Systems Fall 1997
Tools for Z
Garlan Lab 1 Due: Sep 29, 1997
CMU has several tools for manipulating Z descriptions. To access these tools you will need to have an account on a machine that can access MSE-supported software.The tools directory is /usr/misc/.se-support/
The tool you will use to check a Z specification is:
1. fuzz: a type checker for Z. Assumes that your Z description has been written using Latex (see below).. For some examples check out /usr/misc/.se-support/doc/fuzz. You will also find here a tutorial Fuzz_2-o.ps, which contains a guide to using fuzz and the other MSE-supported tools. Print it on any printer to see how to invoke fuzz and the related tools.
To use fuzz you first have to create a document in the Latex format. In addition to your favorite text editor there are three tools that are useful. (These tools are usually found in /usr/local/bin.)
2. latex: a document formatter. Fuzz_2-o.ps explains how to use Latex. Basically, you include "fuzz" in the style header, and then use certain formatting conventions to obtain schemas, and other mathematical symbols.
3. xdvi: a previewer for Latex-generated output.
4. dvips: a tool for printing documents generated by latex.
You can also find some example Latex files in the class directory: /afs/cs/academic/class/15671-f97/examples. You will also find in this directory a file handin.tex, which has a simple Latex template for your homework.
Lab tasks
1. Look through the MSE Facilities Guide to Fuzz.
2. Create a file with some formal text formatted in Latex. Produce a dvi file using latex, preview it with xdvi, and print it on a printer near you.
3. Make a copy of the files: example.tex, tut.tex, and fuzz.sty.
4. Work through the tutorial example in the Fuzz manual using example.tex.
5. Peruse tut.tex and try checking it with the -t switch.