Formal Methods - Z notation
Practical information
Part II 2/CS/3T Unit (Autumn Term)

Lecturer: Jonathan Bowen

Mark Green will be assisting with all practical sessions in general. Simeon Veloudis may help with some practical sessions or stand in for Mark if necessary.

Software tool support

• L^_AT^_EX - a document preparation system, whose input can be type-checked by ZTC. Run using latex. Input files have extension .tex; formatted "DVI" ("DeVice Independent") output files have extension .dvi. A log file with extension .log (including errors if any) is also produced. An auxilary file with extension .aux (for internal information) may be produced as well. View the DVI output file using the xdvi program and print it using dvips (or produce a PostScript file using the -o option that can be printed subsequently).

• ZTC - a Z type-checker which accepts L^ATEX documents as input. Documentation includes a short Unix-style manual page (at the back of your full printed manual) ztc.sty L^ATEX style file which may be used in conjunction with the oz.sty style file, and full documentation (issued in printed form). Run using ztc. A log file with extension .log and a text listing of the types found with extension .typ are produced. (Note possible clash with LaTeX log output above.)

• ZANS - a (prototype) Z animator. Run using zans. For information, see the printed tutorial (to be issued at one of the lectures). Remember ZANS is still under development and thus is not perfect.

setenv PATH "${PATH}:/packages/ztc:/packages/zans:/packages/teTeX/bin/sparc-solaris2.5"

The following will help ZTC find its associated files:

setenv ZMTPATH /packages/ztc

Lines suitable for direct inclusion in your ~/.login file to help set up your environment correctly may be found in the file /home/cs/pub/jpb/z/login . It is recommended you use the textedit window-based editor for editing text files like ~/.login (and LaTeX source files). Include the /home/cs/pub/jpb/z/login file in your ~/.login file at the point where it says you should add your own commands towards the end of the file.

Files for use with this software are available under the directory /home/cs/pub/jpb/z . An example initial Z specification based on Exercise 4 is available as /home/cs/pub/jpb/z/exercise.tex, together with other associated files.

To edit your .login file, make and use a subdirectory called z, copy the example files, LaTeX, view, type-check and produce PostScript formatted output suitable for eventual printing, use the following Unix commands:

cd
textedit .login &
mkdir z
cd z
cp /home/cs/pub/jpb/z/* .
source login

latex exercise
xdvi exercise &
ztc exercise.tex -T
dvips exercise -o

(Make sure you include the -o option for the dvips command above. Otherwise you will print the file!) A file called README includes further information on the various files in the /home/cs/pub/jpb/z directory, which includes a number of example specifications as well as exercise.tex. Check that all the commands above work. Note that exercise.tex will not type-check correctly as it stands. Look at the files in the directory using the Solaris window system File Manager accessible from the main window Workspace Menu (or using the Unix ls command). You may view (and/or edit) files by clicking on them in a File Manager window (or using the Unix more command). For Unix manual pages on individual commands, use "man command".

Copy the example file to another file and edit it to start creating your own Z specification and report:

cp exercise.tex pract.tex
textedit pract.tex &

To print a PostScript file on the "lw1" printer (for example), use the following command:

lpr -Plw1 pract.ps

It is recommended you do not actually do this (to save your printer quota) until you need to print your final assessment report. You may use xdvi to view your formatted Z specification in a window on the screen at any time.

Note: If you use a Computer Services Centre Sun workstation, you will probably need to rlogin to the Department of Computer Science saturn Sun server to run latex, ZTC, ZANS, etc.

Practical overview

Practical 1: (Week 4)

Beforehand: complete Exercise 4 (except the last question which is optional).

Bring your initial hand-written Z specification to the practical and show it to the demonstrator. Ensure you are signed off on the register.

Outcome: set up and use LaTeX, XDVI view, ZTC type-checker, etc.

Practical 2: (Week 5)

Beforehand: create your initial specification using a text editor.

Outcome: enter your initial specification (e.g., the abstract state and - at least three - successful operations) and type-check it.

Optional: include axiomatic and/or generic definitions if required.

Practical 3: (Week 6)

Beforehand: add draft English comments to your specification and update it.

Outcome: add error reports and total operations and type-check your revised specification.

Optional: add hypotheses or theorems with proofs about your specification.

Practical 4: (Week 7)

Beforehand: ensure your specification is acceptable to both LaTeX and ZTC.

Outcome: polish your specification and English explanation ready for demonstration, ensuring it still type-checks correctly. In particular, check all your preconditions and that you have considered the change of state for all parts of your abstract state.

Show your type-checked specification to the demonstrator using XDVI, and show ZTC processing it at your practical session. Ensure you are signed off on the register.

Practical 5: (Week 8)

Beforehand: study the ZANS tutorial (to be issued in lectures).

Outcome: use ZANS animator on an updated version of your specification. Add Introduction, ZANS and Conclusion sections to your report.

Write-up: (Week 9)

Polish, complete, format and print your report.

Outcome: hand your completed report into the Porter's Lodge.

Deadline (Friday, 3rd December):

If you find anything above unclear, please contact the demonstrator or me and we will attempt to remedy the problem.