From RM@uk.mod.rsre Wed Jan 4 00:59:28 1989 Return-Path: From: Ruaridh Macdonald (on UK.MOD.RSRE) To: Z2@uk.mod.rsre, ZLOCAL@uk.mod.rsre Date: Tue, 3 Jan 89 11:26 Subject: Z Forum Issue 4.1 Acknowledge-To: RM%uk.mod.rsre@uk.ac.ucl.cs.ess Message-Id: <03 JAN 1989 11:26:02 RM@RSRE> 3rd January 1989 Z FORUM Volume 4 Issue 1 ---------------- ------- ---------------- Today's Topics -------------- Z Bibliography on the PRG Archive Server Course: Z for Engineers The FUZZ Type-Checker --------------------------------------------------------------------- The last issue of Volume 3 was number 8. --------------------------------------------------------------------- Date: Tue, 20 Dec 88 18:08:16 GMT From: bowen@uk.ac.oxford.prg Subject: Z Bibliography on the PRG archive server I have installed this on the PRG archive server as "zbib" (i.e. send a command of "send z zbib" via e-mail to on JANET retrieve it). It is in UNIX refer database format. Also installed are: zselectbib like "zbib" but only selected publications (as distributed at the 1988 Z Users Meeting) zbib.roff a formatted version of "zbib" zselectbib.roff a formatted version of "zselectbib" For help on using the archive server, send a message containing the command "help". For an index of Z related documents, send a command of "index z". The LaTeX files related to the Z bibliography on the archive server are still the old versions. I may update these in the future if and when I have time. -- Jonathan (Bowen) Programming Research Group --------------------------------------------------------------------- From: DillerAR@uk.ac.birmingham.computer-science Date: Thu, 22 Dec 88 10:40:48 GMT Subject: Course: Z for Engineers University of Birmingham School of Electronic and Electrical Engineering Z FOR ENGINEERS (Preliminary Announcement) 3-6 July 1989 The object of this course is to give a thorough grounding in the formal definition language Z and its application. It will enable existing Z specifications to be read and small ones to be constructed, and provide an understanding of the methods employed in reasoning about formal specifications. Topics include an introduction to formal methods, the mathematical toolkit, the schema calculus, theorems and proofs and operational decomposition. ORGANISED JOINTLY BETWEEN THE SCHOOL OF ELECTRONIC AND ELECTRICAL ENGINEERING AND THE SCHOOL OF COMPUTER SCIENCE Further information may be obtained from: Mrs B. Skerratt, The Post Experience Courses Secretary, School of Engineering Production, University of Birmingham, P.O Box 363, Birmingham, B15 2TT. Telephone: 021--414--4305. --------------------------------------------------------------------- Date: Tue, 13 Dec 88 11:38:16 GMT From: Mike Spivey Subject: The FUZZ Type-Checker THE FUZZ TYPE-CHECKER Mike Spivey I have recently been working on a type checker for Z, which goes by the name of `fuzz' (by analogy with the UNIX tool `lint' for checking C programs). I originally developed it to check the Z Reference Manual, and I have now packaged it up and documented it. One part of the fuzz package is a LaTeX document style option. This is an improved version of the `zed.sty' I made available some time ago, and is broadly compatible with it. Specifications can be entered as ordinary ASCII files using a text editor, then LaTeX and the fuzz style option can be used to prepare them for printing on a wide range of laser printers and photo-typesetters. This style option has been used to for at least three published books on Z. The new style option comes with its own font of special symbols. Here is an example of the input format: \documentstyle[fuzz]{article} \begin{document} Let $PERSON$ be the set of all people: \begin{zed} [PERSON]. \end{zed} A `club' has a set of members and a president, who must be a member: \begin{schema}{Club} members: \power PERSON \\ president: PERSON \where president \subseteq members \end{schema} To enroll somebody in the club, we just add them to the set of members: \begin{schema}{Enroll} \Delta Club \\ new?: PERSON \where members' = members \cup new? \\ president' = president \end{schema} The president doesn't change when a new member is enrolled. \end{document} Sorry, but I can't do justice to the high-quality printed output here! The type checker itself works on the same file of text as LaTeX. It extracts the formal text of the specification and checks it for conformance with the rules of the Z language, as documented in the Z Reference Manual. Analysis of a 1300-line specification takes about 7 seconds on a SUN 3/75. Here are the error messages the type checker produces when run on the specification above, which contains two deliberate mistakes: "example.tex", line 12: Type mismatch in left argument of infix relation > Predicate: president \subseteq members > Arg type: PERSON > Expected: P ? "example.tex", line 20: Argument 2 has wrong type > Expression: (members \cup new?) > Arg 2 type: PERSON > Expected: P PERSON Each error message is supported by corroborative detail about the expressions involved and their types. As an option, the type checker will produce a report listing all the names defined in the specification. Here is the listing for our example specification: Given PERSON Schema Club members: P PERSON president: PERSON End Schema \Delta Club members: P PERSON president: PERSON members': P PERSON president': PERSON End Schema Enroll members: P PERSON president: PERSON members': P PERSON president': PERSON new?: PERSON End Each schema is shown with an expanded list of its components, which is useful in understanding a large specification. The fuzz distribution contains the LaTeX style option, a special font of Z symbols, object code for the analysis program, a library containing the standard mathematical tool-kit, and some example specifications. To use fuzz, you will need to have LaTeX installed on your machine, but everything else you need is in the distribution. It will be available in early January under `no-nonsense' licence conditions for the IBM PC and other MS-DOS machines, and for the SUN under SUN UNIX. The PC version can also be used on the PS/2. Versions for other machines may be available according to demand. You can order the fuzz package either by cutting out the coupon below and sending it with your payment, or by sending an official order. Please send all orders to: Mrs. A. Spivey, 34, Westlands Grove, Stockton Lane, York, YO3 0EF. Technical enquiries can be sent to me at: 2, Willow Close, Garsington, Oxford, OX9 9AN, or mike@uk.ac.oxford.prg . -- Mike Spivey. ----8<--------8<--------8<--------8<--------8<--------8<--------8<---- FUZZ PACKAGE: ORDER FORM Name: ________________________________________ Address: ________________________________________ ________________________________________ ________________________________________ Please send [ ] copies of the `fuzz' package for the following machines: [ ] SUN version: Cartridge tape 300 pounds [ ] IBM PC version: 5.25in disk 200 pounds [ ] IBM PC version: 3.5in disk 200 pounds -- subject to a 2 week delay I enclose a cheque for [ ] pounds, payable to Dr. J. M. Spivey. Signed: ____________________ --------------------------------------------------------------------- *************************** END OF Z FORUM 4.1 **********************