From csus.edu!csulb.edu!news.sgi.com!news.mathworks.com!EU.net!usenet2.news.uk.psi.net!uknet!usenet1.news.uk.psi.net!uknet!uknet!lyra.csx.cam.ac.uk!news.ox.ac.uk!zforum-request Sun Oct 13 08:29:20 1996 Path: csus.edu!csulb.edu!news.sgi.com!news.mathworks.com!EU.net!usenet2.news.uk.psi.net!uknet!usenet1.news.uk.psi.net!uknet!uknet!lyra.csx.cam.ac.uk!news.ox.ac.uk!zforum-request From: zforum-request@comlab.ox.ac.uk Newsgroups: comp.specification.z,comp.specification.misc,comp.answers,news.answers Subject: comp.specification.z Frequently Asked Questions (Monthly) Supersedes: Followup-To: comp.specification.z Date: Fri, 4 Oct 1996 08:35:33 GMT Organization: Z User Group Lines: 431 Sender: bowen@comlab.ox.ac.uk (Jonathan Bowen) Approved: news-answers-request@MIT.Edu Message-ID: Reply-To: J.P.Bowen@reading.ac.uk NNTP-Posting-Host: gruffle.comlab.ox.ac.uk Summary: Information about the Z formal specification notation Originator: bowen@gruffle.comlab Xref: csus.edu comp.specification.z:2593 comp.specification.misc:736 comp.answers:21638 news.answers:83914 Status: O Archive-name: z-faq Last-modified: 30 September 1996 Maintainer: Jonathan Bowen URL: ftp://ftp.comlab.ox.ac.uk/pub/Zforum/faq NAME: comp.specification.z STATUS: unmoderated PURPOSE: Discussion concerning the formal specification notation Z. (If you have read this before, changed and new sections since the previously issued version are marked with `|' in the left hand margin.) Questions have been marked with "Subject:" at the start of the line to allow some newsreaders to scan them easily (e.g., "^G" within "rn"). Subject: What is it? Z (pronounced `zed') is a formal specification notation based on set theory and first order predicate logic. It has been developed at the Programming Research Group at the Oxford University Computing Laboratory (OUCL) and elsewhere since the late 1970s. It is used by industry as part of the software (and hardware) development process in Europe, USA and elsewhere. Currently it is undergoing international ISO standardization. The comp.specification.z electronic USENET newsgroup was established in June 1991 and is intended to handle messages concerned with Z. It has an estimated readership of around 30,000 people worldwide. Comp.specification.z provides a convenient forum for messages concerned with recent developments and the use of Z. Pointers to and reviews of recent books and articles are particularly encouraged. These may be included in the Z bibliography (see below) if they appear in comp.specification.z. Subject: What if I know someone interested without access to USENET news? There is an associated Z FORUM electronic mailing list that was initiated in January 1986 by Ruaridh Macdonald, RSRE, UK. Articles are now automatically cross-posted between comp.specification.z and the mailing list for those whose do not have access to USENET news. This may apply especially to industrial Z users who are particularly encouraged to subscribe and post their experiences to the list. Please contact with your name, address and email address to join the mailing list (or if you change your email address or wish to be removed from the list). Readers are strongly urged to read the comp.specification.z newsgroup rather than the Z FORUM mailing list if possible. Messages for submission to the Z FORUM mailing list and the comp.specification.z newsgroup may be emailed to . This method of posting is particularly recommended for important messages like announcements of meetings since not all messages posted on comp.specification.z reach the OUCL. A mailing list for the Z User Meeting educational issues session has been set by Neville Dean, Anglia Polytechnic University, UK. Anyone interested may join by emailing with your contact details. A specialist electronic mailing for discussion of SAZ, a combination of the structured method SSADM and Z existed for a while, but is now closed. Subject: What if I know someone interested without access to email? If you wish to join the postal Z mailing list, please send your address to Amanda Kingscote, Praxis plc, 20 Manvers Street, Bath BA1 1PX, UK (tel +44-1225-444700, fax +44-1225-465205, email ). This will ensure you receive details of Z meetings, etc., particularly for people without access to electronic mail. Subject: How can I join in? If you are currently using Z, you are welcome to introduce yourself to the newsgroup and Z FORUM list by describing your work with Z or raising any questions you might have about Z which are not answered here. You may also advertize publications concerning Z which you or your colleagues produce. These may then be added to the master Z bibliography maintained at the OUCL (see below). Subject: Where are Z-related files archived? Information on the World Wide Web (WWW) is available under the http://www.comlab.ox.ac.uk/archive/z.html page. See also the http://www.comlab.ox.ac.uk/archive/formal-methods.html page on formal methods in general. The WWW global hypertext system is accessible using the "netscape", "mosaic" or "lynx" programs for example. Contact your system manager if WWW access is not available on your system. Some of the archive is also available via anonymous FTP on the Internet under the ftp://ftp.comlab.ox.ac.uk/pub/Zforum directory. Type the command "ftp ftp.comlab.ox.ac.uk" (or alternatively "ftp 163.1.27.2" if this does not work) and use "anonymous" as the login id and your email address as the password when prompted. The FTP command "cd pub/Zforum" will get you into the Z archive directory. The file ftp://ftp.comlab.ox.ac.uk/pub/Zforum/README gives some general information and ftp://ftp.comlab.ox.ac.uk/pub/Zforum/00index gives a list of the files. (Retrieve these using the FTP command "get README", for example.) There is an automatic electronic mail-based electronic archive server which allows access to some of the archive such as most messages on comp.specification.z and Z FORUM, as well as a selection of other Z-related text files. Send an email message containing the command "help" to for further information on how to use the server. A command of "index z" will list the Z-related files. To receive files via email, send a message containing the command "send z ..." to . If you have serious trouble accessing the archive server, please contact the address . Subject: What tools are available? Various tools for formatting, type-checking and aiding proofs in Z are available. A free LaTeX style file and documentation can be obtained from the OUCL archive. Access the ftp://ftp.comlab.ox.ac.uk/pub/Zforum/zed.sty and ftp://ftp.comlab.ox.ac.uk/pub/Zforum/zguide.tex files. A newer style "csp_zed.sty" is available in the same location, which uses the new font selection scheme and covers CSP and Z symbols. A style for Object-Z "oz.sty" with a guide "oz.tex" is also accessible. LaTeX2e users may find "zed-csp.sty" and "zed2e.tex" useful. The fuzz package, a syntax and type-checker with a LaTeX style option and fonts, is available from the Spivey Partnership, 10 Warneford Road, Oxford OX4 1LU, UK. It is compatible with the 2nd edition of Spivey's Z Reference Manual. Access ftp://ftp.comlab.ox.ac.uk/pub/Zforum/fuzz for brief information and an order form. Contact Mike Spivey (email ) for further information. CADiZ is a suite of integrated tools for preparing and type-checking Z specifications as professional quality typeset documents. The Z dialect it recognizes is evolving in line with the standard. The typesetting can be performed by either troff or LaTeX for Unix or Word for Windows. The mouse can be used to interact with a view of the typeset specification to inspect properties deduced by the type-checker, to see the expansion of schema calculus expressions, and to reason about conjectures such as proof obligations. The PC version is integrated with MS Word using OLE2, providing WYSIWYG editing of Z paragraphs directly in Word documents. (The troff and LaTeX versions use ordinary text editors on ASCII mark-up.) Further development of the tools is ongoing. CADiZ is a BCS Award winning product available for Sun, SGI and PC machines from York Software Engineering Ltd, The Innovation Centre, York Science Park, Heslington, York, YO1 5DG, UK (email yse@minster.york.ac.uk, tel +44-1904-435206, fax +44-1904-435135). ProofPower is a suite of tools supporting specification and proof in Higher Order Logic (HOL) and in Z. Short courses on ProofPower-Z are available as demand arises. Information about ProofPower can be obtained automatically by sending email to . Contact Roger Jones, International Computers Ltd, Eskdale Road, Winnersh, Wokingham, Berkshire RG11 5TT, UK (tel +44-118-969-3131 ext 6536, fax +44-118-969-7636, email ) for further details. Zola is a commercial integrated support tool for Z on Sun workstations, for automated assistance at all stages of the specification construction, proving and maintenance process. It is intended for system developers and includes a WYSIWYG editor, type-checker and tactical theorem prover suitable for the creation and maintenance of large specifications. For further information, contact Chris Paine or Will Harwood, Imperial Software Technology, 62-74 Burleigh Street, Cambridge CB1 1DJ, UK (tel +44-1223-462400, fax +44-1223-462500, email ). ZTC is a Z type-checker available free of charge for educational and non-profit uses. It is intended to be compliant with the 2nd edition of Spivey's Z Reference Manual. It accepts LaTeX with "zed" or "oz" styles, and ZSL - an ASCII version of Z. ZANS is a Z animator. It is a research prototype that is still very crude. Both ZTC and ZANS run on Linux, SunOS 4.x, Solaris 2.x, HP-UX 9.0, DOS, and extended DOS. They are available via anonymous FTP under ftp://ise.cs.depaul.edu/pub in the directories ZANS-x.xx and ZTC-x.xx, where x.xx are version numbers. Contact Xiaoping Jia for further information. Formaliser is a syntax-directed WYSIWYG Z editor and interactive type checker, running under Microsoft Windows, available from Logica. Contact Susan Stepney, Logica UK Limited, Cambridge Division, Betjeman House, 104 Hills Road, Cambridge CB2 1LQ, UK (tel +44-1223-366343, fax +44-1223-251001, email ) or see under http://public.logica.com/~formaliser/formlsr/formlsr.htm on-line. DST-fuzz is a set of tools based on the fuzz package by Mike Spivey, supplying a Motif based user interface for LaTeX based pretty printing, syntax and type-checking. A CASE tool interface allows basic functionality for combined application of Z together with structured specifications. The tools are integrated into SoftBench. For further information contact Hans-Martin Hoercher, DST Deutsche System-Techik GmbH, Edisonstr. 3, D-24145 Kiel, Germany (tel +49-431-7109-478, fax +49-431-7109-503, email ). The B-Tool can be used to check proofs concerning parts of Z specifications. This is licensed by Edinburgh Portable Compilers Ltd, 17 Alva Street, Edinburgh EH2 4PH, UK (tel +44-131-225-6262, fax +44-131-225-6644). Contact the Distribution Manager (email ) for further information. The B-Toolkit is a set of integrated tools which fully supports the B-Method for formal software development and is available from B-Core (UK) Limited, Magdalen Centre, The Oxford Science Park, Oxford OX4 4GA, UK. For further details, contact Ib Sorensen (tel +44-1865-784520, fax +44-1865-784518, email ) or see http://www-scm.tees.ac.uk/bresource/docs/B/btoolkit.html on-line. Z fonts for MS Windows and Macintosh are available on-line. For hyperlinks to these and other Z tool resources see the WWW Z page: http://www.comlab.ox.ac.uk/archive/z.html#tools A survey of Z tools (produced in 1991) may be obtained from Colin Parker, Systems Process Department, W376C, British Aerospace, Warton Aerodrome, Warton, Preston PR4 1AX, UK. Subject: How can I learn about Z? There are a number of courses on Z run by industry and academia. Oxford University offers industrial short courses in the use Z. As well as introductory courses, recent newly developed material includes advanced Z-based courses on proof and refinement, partly based around the B-Tool. Courses are held in Oxford, or elsewhere (e.g., on a company's premises) if there is enough demand. For further information, contact Jim Woodcock (tel +44-1865-283514, fax +44-1865-273839, email ). Logica offer a five day course on Z at company sites. Contact Rosalind Barden (tel +44-1223-366343 ext 4860, fax +44-1223-322315, email ) at Logica UK Limited, Betjeman House, 104 Hills Road, Cambridge CB2 1LQ, UK. Praxis Systems plc runs a range of Z (and other formal methods) courses. For details contact Anthony Hall on +44-1225-444700 or . Formal Systems (Europe) Ltd run a range of Z, CSP and other formal methods courses, primarily in the US and with such lecturers as Jim Woodcock and Bill Roscoe (both lecturers at the OUCL). For dates and prices contact Kate Pearson (tel +44-1865-728460, fax +44-1865-201114) at Formal Systems (Europe) Limited, 3 Alfred Street, Oxford OX1 4EH, UK. DST Deutsche System-Technik runs a collection of courses for either Z or CSP, mainly in Germany. These courses range from half day introductions to formal methods and Z to one week introductory or advanced courses, held either at DST, or elsewhere. For further information contact Hans-Martin Hoercher, DST Deutsche System-Techik GmbH, Edisonstr. 3, D-24145 Kiel, Germany (tel +49-431-7109-478, fax +49-431-7109-503, email ). Subject: What has been published about Z? A searchable on-line Z bibliography is available on the World Wide Web under http://www.comlab.ox.ac.uk/archive/z/bib.html in BibTeX format. For those without WWW access, an older compressed version is available under ftp://ftp.comlab.ox.ac.uk/pub/Zforum/z.bib.Z (and also ftp://ftp.comlab.ox.ac.uk/pub/Zforum/z.ps.Z in PostScript format). Information on OUCL Technical Monographs and Reports, including many on Z, is available from the librarian (tel +44-1865-273837, fax +44-1865-273839, email ). "Formal Methods: A Survey" by S.Austin & G.I.Parkin, March 1993 includes information on the use and teaching of Z in industry and academia. Contact DITC Office, Formal Methods Survey, National Laboratory, Teddington, Middlesex TW11 0LW, UK (tel +44-181-943-7002, fax +44-181-977-7091) for a copy. The following books largely concerning Z have been or are due to be published (in approximate chronological order): I.Hayes (ed.), Specification Case Studies, Prentice Hall International Series in Computer Science, 1987. (2nd ed., 1993) | URL: http://www.prenhall.com/013/832543/ptr/83254-3.html J.M.Spivey, Understanding Z: A specification language and its formal semantics, Cambridge University Press, 1988. D.Ince, An Introduction to Discrete Mathematics, Formal System Specification and Z, Oxford University Press, 1988. (2nd ed., 1993) J.C.P.Woodcock & M.Loomes, Software Engineering Mathematics: Formal Methods Demystified, Pitman, 1998. (Also Addision-Wesley, 1989) J.M.Spivey, The Z Notation: A reference manual, Prentice Hall International Series in Computer Science, 1989. (2nd ed., 1992) [Widely used as a de facto standard for Z. Often known as ZRM2.] A.Diller, Z: An introduction to formal methods, Wiley, 1990. J.E.Nicholls (ed.), Z user workshop, Oxford 1989, Springer-Verlag, Workshops in Computing, 1990. B.Potter, J.Sinclair & D.Till, An Introduction to Formal Specification and Z, Prentice Hall International Series in Computer Science, 1991. | (2nd ed., due 1996) | URL: http://www.prenhall.com/013/242206/ptr/24220-6.html D.Lightfoot, Formal Specification using Z, MacMillan, 1991. A.Norcliffe & G.Slater, Mathematics for Software Construction, Ellis Horwood, 1991. J.E.Nicholls (ed.), Z User Workshop, Oxford 1990, Springer-Verlag, Workshops in Computing, 1991. I.Craig, The Formal Specification of Advanced AI Architectures, Ellis Horwood, 1991. M.Imperato, An Introduction to Z, Chartwell-Bratt, 1991. J.B.Wordsworth, Software Development with Z, Addison-Wesley, 1992. S.Stepney, R.Barden & D.Cooper (eds.), Object Orientation in Z, Springer-Verlag, Workshops in Computing, August 1992. URL: http://public.logica.com/~stepneys/bib/ss/ooz.htm J.E.Nicholls (ed.), Z User Workshop, York 1991, Springer-Verlag, Workshops in Computing, 1992. URL: http://www.imi.gla.ac.uk/springer/eWiC/Abstracts/9.html D.Edmond, Information Modeling: Specification and implementation, Prentice Hall, 1992. J.P.Bowen & J.E.Nicholls (eds.), Z User Workshop, London 1992, Springer-Verlag, Workshops in Computing, 1993. URL: http://www.comlab.ox.ac.uk/archive/z/zum92.html S.Stepney, High Integrity Compilation: A case study, Prentice Hall, 1993. URL: http://public.logica.com/~stepneys/bib/ss/hic.htm M.McMorran & S.Powell, Z Guide for Beginners, Blackwell Scientific, 1993. K.C.Lano & H.Haughton (eds.), Object-oriented Specification Case Studies, Prentice Hall International Object-Oriented Series, 1993. B.Ratcliff, Introducing Specification using Z: A practical case study approach, McGraw-Hill, 1994. A.Diller, Z: An introduction to formal methods, 2nd ed., Wiley, 1994. J.P.Bowen & J.A.Hall (eds.), Z User Workshop, Cambridge 1994, Springer-Verlag, Workshops in Computing, 1994. URL: http://www.comlab.ox.ac.uk/archive/z/zum94.html R.Barden, S.Stepney & D.Cooper, Z in Practice, Prentice Hall BCS Practitioner Series, 1994. URL: http://public.logica.com/~stepneys/bib/ss/zip.htm D.Rann, J.Turner & J.Whitworth, Z: A beginner's guide. Chapman & Hall, 1994. D.Heath, D.Allum & L.Dunckley, Introductory Logic and Formal Methods. A.Waller, Henley-on-Thames, 1994. L.Bottaci and J.Jones, Formal Specification using Z: A modelling approach. International Thomson Publishing, 1995. D.Sheppard, An Introduction to Formal Specification with Z and VDM. McGraw Hill International Series in Software Engineering, 1995. J.P.Bowen & M.G.Hinchey (eds.), ZUM'95: The Z Formal Specification Notation, Springer-Verlag, Lecture Notes in Computer Science, volume 967, 1995. URL: http://www.comlab.ox.ac.uk/archive/z/zum95.html J.P.Bowen, Formal Specification and Documentation using Z: A Case Study Approach, International Thomson Compress Press, 1996. URL: http://www.comlab.ox.ac.uk/oucl/users/jonathan.bowen/zbook.html J.C.P.Woodcock & J.Davies, Using Z: Specification, proof and refinement, Prentice Hall International Series in Computer Science, 1996. URL: http://www.comlab.ox.ac.uk/usingz.html | A.Harry, Formal Methods Fact File: VDM and Z, Wiley, 1996. Announced: J.Jacky, The Way of Z: Formal Methods Demystified, Cambridge University Press, November 1996. L.Semmens, Z for Software Engineers, Ellis Horwood Series in Computers and Their Applications, December 1996. See also an on-line list of Z books from Blackwells Bookshop under: http://www.blackwell.co.uk/cgi-bin/bb_catsel?09_IBY Subject: What is object-oriented Z? Several object-oriented extensions to or versions of Z have been proposed. The book "Object orientation in Z", listed above, is a collection of papers describing various OOZ approaches - Hall, ZERO, MooZ, Object-Z, OOZE, Schuman&Pitt, Z++, ZEST and Fresco (an OO VDM method) - in the main written by the methods' inventors, and all specifying the same two examples. A more recent book entitled "Object-oriented specification case studies" surveys the principal methods and languages for formal object-oriented specification, including Z-based approaches. Subject: How can I run Z? Z is a (non-executable in general) specification language, so there is no such thing as a Z compiler/linker/etc. as you would expect for a programming language. Some people have looked at animating subsets of Z for rapid prototyping purposes, using logic and functional programming for example, but this work is preliminary and is not really the major point of Z, which is to increase human understandability of the specified system and allow the possibility of formal reasoning and development. However, Prolog seems to be the main favoured language for Z prototyping and some references may be found in the Z bibliography (see above). Subject: Where can I meet other Z people? The 10th International Conference of Z Users (ZUM'97) will be held 3-4 April 1997 at the University of Reading, UK. For general enquiries, contact the Conference Chair, Jonathan Bowen (tel +44-118-931-6544, fax +44-118-975-1994, email ). Information on ZUM'97 is available under http://www.cs.reading.ac.uk/archive/z/zum97/ via WWW. Information on Z User Meetings is issued on newsgroups including comp.specification.z, the Z postal mailing list and various specialist electronic mailing lists. The 9th International Conference of Z Users (ZUM'95) was held 7-9 September 1995 in Limerick, Ireland. The proceedings appeared in the Springer-Verlag LNCS series (volume 967). Previous proceedings for Z User Meetings have been published in the Springer-Verlag Workshops in Computing series since the 4th meeting in 1989. See the URL http://www.comlab.ox.ac.uk/archive/z/zum.html for further on-line information on previous meetings. For a list of meetings with a formal methods content, see: http://www.comlab.ox.ac.uk/archive/formal-methods/meetings.html Subject: What is the Z User Group? The Z User Group was set up in 1992 to oversee Z-related activities, and the Z User Meetings in particular. As a subscriber to either comp.specification.z, ZFORUM or the postal mailing list, you may consider yourself a member of the Z User Group. There are currently no charges for membership, although this is subject to review if necessary. Contact for further information. Subject: How can I obtain the draft Z standard? The proposed Z standard under ISO/IEC JTC1/SC22 is available electronically via anonymous FTP *only* (not via the mail server since it is too large) from the Z archive at Oxford in compressed PostScript format. Version 1.0 of the draft standard is accessible as the file ftp://ftp.comlab.ox.ac.uk/pub/Zforum/zstandard1.0.ps.Z together with an annex in ftp://ftp.comlab.ox.ac.uk/pub/Zforum/zstandard-annex1.0.ps.Z It is also available in printed form from the OUCL librarian (tel +44-1865-273837, fax +44-1865-273839, email ) by requesting Technical Monograph number PRG-107. Subject: Where else is Z discussed? The BCS-FACS (British Computer Society Formal Aspects of Computer Science special interest group) and FME (Formal Methods Europe) are two organizations interested in formal methods in general. Contact BCS FACS, Dept of Computer Studies, Loughborough University of Technology, Loughborough, Leicester LE11 3TU, UK (tel +44-1509-222676, fax +44-1509-211586, email ) for further information. A "FACS Europe" newsletter is issued to members of FACS and FME. Please send suitable Z-related material to the Z column editor, David Till, Dept of Computer Science, City University, Northampton Square, London, EC1V 0HB, UK (tel +44-171-477-8552, email ) for possible publication. Material from articles appearing on the comp.specification.z newsgroup may be included if considered of sufficient interest (with permission from the originator if possible). It would be helpful for posters of articles on comp.specification.z to indicate if they do not want further distribution for any reason. Subject: How does VDM compare with Z? See I.J.Hayes, C.B.Jones & J.E.Nicholls, Understanding the differences between VDM and Z, FACS Europe, series I, 1(1):7-30, Autumn 1993 available as an on-line Technical Report from Manchester under ftp://ftp.cs.man.ac.uk/pub/TR/UMCS-93-8-1.ps.Z and I.J.Hayes, VDM and Z: A comparative case study, Formal Aspects of Computing, 4(1):76-99, 1992. VDM is discussed on the (unmoderated) VDM FORUM mailing list. Send a message containing the command "join vdm-forum " where is your real name to . To contact the list administrator, email John Fitzgerald on . |Subject: How does the B-Method compare with Z? | |See http://www.b-core.com/ZVdmB.html for a comparison. See also |http://www.comlab.ox.ac.uk/archive/formal-methods/b.html for further |information on B. Subject: What if I have spotted a mistake or an omission? Please send corrections or new relevant information about meetings, |books, tools, etc., to . New questions and model answers are also gratefully received! -- Jonathan Bowen Department of Computer Science, University of Reading, UK URL: http://www.cs.reading.ac.uk/people/jpb/ From csus.edu!csulb.edu!news.sgi.com!howland.erols.net!newsfeed.internetmci.com!in1.uu.net!EU.net!usenet2.news.uk.psi.net!uknet!usenet1.news.uk.psi.net!uknet!uknet!bhamcs!news.ox.ac.uk!zforum-request Fri Nov 1 07:11:42 1996 Path: csus.edu!csulb.edu!news.sgi.com!howland.erols.net!newsfeed.internetmci.com!in1.uu.net!EU.net!usenet2.news.uk.psi.net!uknet!usenet1.news.uk.psi.net!uknet!uknet!bhamcs!news.ox.ac.uk!zforum-request From: zforum-request@comlab.ox.ac.uk Newsgroups: comp.specification.z,comp.specification.misc,comp.answers,news.answers Subject: comp.specification.z Frequently Asked Questions (Monthly) Supersedes: Followup-To: comp.specification.z Date: Fri, 1 Nov 1996 02:00:07 GMT Organization: Z User Group Lines: 434 Sender: news@comlab.ox.ac.uk (News) Approved: news-answers-request@MIT.Edu Expires: Fri, 13 Dec 1996 02:00:01 GMT Message-ID: Reply-To: J.P.Bowen@reading.ac.uk NNTP-Posting-Host: gruffle.comlab.ox.ac.uk Summary: Information about the Z formal specification notation Originator: news@gruffle.comlab Xref: csus.edu comp.specification.z:2625 comp.specification.misc:781 comp.answers:22217 news.answers:86139 Archive-name: z-faq Last-modified: 14 October 1996 Maintainer: Jonathan Bowen URL: ftp://ftp.comlab.ox.ac.uk/pub/Zforum/faq NAME: comp.specification.z STATUS: unmoderated PURPOSE: Discussion concerning the formal specification notation Z. (If you have read this before, changed and new sections since the previously issued version are marked with `|' in the left hand margin.) Questions have been marked with "Subject:" at the start of the line to allow some newsreaders to scan them easily (e.g., "^G" within "rn"). Subject: What is it? Z (pronounced `zed') is a formal specification notation based on set theory and first order predicate logic. It has been developed at the Programming Research Group at the Oxford University Computing Laboratory (OUCL) and elsewhere since the late 1970s. It is used by industry as part of the software (and hardware) development process in Europe, USA and elsewhere. Currently it is undergoing international ISO standardization. The comp.specification.z electronic USENET newsgroup was established in June 1991 and is intended to handle messages concerned with Z. It has an estimated readership of around 30,000 people worldwide. Comp.specification.z provides a convenient forum for messages concerned with recent developments and the use of Z. Pointers to and reviews of recent books and articles are particularly encouraged. These may be included in the Z bibliography (see below) if they appear in comp.specification.z. Subject: What if I know someone interested without access to USENET news? There is an associated Z FORUM electronic mailing list that was initiated in January 1986 by Ruaridh Macdonald, RSRE, UK. Articles are now automatically cross-posted between comp.specification.z and the mailing list for those whose do not have access to USENET news. This may apply especially to industrial Z users who are particularly encouraged to subscribe and post their experiences to the list. Please contact with your name, address and email address to join the mailing list (or if you change your email address or wish to be removed from the list). Readers are strongly urged to read the comp.specification.z newsgroup rather than the Z FORUM mailing list if possible. Messages for submission to the Z FORUM mailing list and the comp.specification.z newsgroup may be emailed to . This method of posting is particularly recommended for important messages like announcements of meetings since not all messages posted on comp.specification.z reach the OUCL. A mailing list for the Z User Meeting educational issues session has been set by Neville Dean, Anglia Polytechnic University, UK. Anyone interested may join by emailing with your contact details. A specialist electronic mailing for discussion of SAZ, a combination of the structured method SSADM and Z existed for a while, but is now closed. Subject: What if I know someone interested without access to email? If you wish to join the postal Z mailing list, please send your address to Amanda Kingscote, Praxis plc, 20 Manvers Street, Bath BA1 1PX, UK (tel +44-1225-444700, fax +44-1225-465205, email ). This will ensure you receive details of Z meetings, etc., particularly for people without access to electronic mail. Subject: How can I join in? If you are currently using Z, you are welcome to introduce yourself to the newsgroup and Z FORUM list by describing your work with Z or raising any questions you might have about Z which are not answered here. You may also advertize publications concerning Z which you or your colleagues produce. These may then be added to the master Z bibliography maintained at the OUCL (see below). Subject: Where are Z-related files archived? Information on the World Wide Web (WWW) is available under the http://www.comlab.ox.ac.uk/archive/z.html page. See also the http://www.comlab.ox.ac.uk/archive/formal-methods.html page on formal methods in general. The WWW global hypertext system is accessible using the "netscape", "mosaic" or "lynx" programs for example. Contact your system manager if WWW access is not available on your system. Some of the archive is also available via anonymous FTP on the Internet under the ftp://ftp.comlab.ox.ac.uk/pub/Zforum directory. Type the command "ftp ftp.comlab.ox.ac.uk" (or alternatively "ftp 163.1.27.2" if this does not work) and use "anonymous" as the login id and your email address as the password when prompted. The FTP command "cd pub/Zforum" will get you into the Z archive directory. The file ftp://ftp.comlab.ox.ac.uk/pub/Zforum/README gives some general information and ftp://ftp.comlab.ox.ac.uk/pub/Zforum/00index gives a list of the files. (Retrieve these using the FTP command "get README", for example.) There is an automatic electronic mail-based electronic archive server which allows access to some of the archive such as most messages on comp.specification.z and Z FORUM, as well as a selection of other Z-related text files. Send an email message containing the command "help" to for further information on how to use the server. A command of "index z" will list the Z-related files. To receive files via email, send a message containing the command "send z ..." to . If you have serious trouble accessing the archive server, please contact the address . Subject: What tools are available? Various tools for formatting, type-checking and aiding proofs in Z are available. A free LaTeX style file and documentation can be obtained from the OUCL archive. Access the ftp://ftp.comlab.ox.ac.uk/pub/Zforum/zed.sty and ftp://ftp.comlab.ox.ac.uk/pub/Zforum/zguide.tex files. A newer style "csp_zed.sty" is available in the same location, which uses the new font selection scheme and covers CSP and Z symbols. A style for Object-Z "oz.sty" with a guide "oz.tex" is also accessible. LaTeX2e users may find "zed-csp.sty" and "zed2e.tex" useful. The fuzz package, a syntax and type-checker with a LaTeX style option and fonts, is available from the Spivey Partnership, 10 Warneford Road, Oxford OX4 1LU, UK. It is compatible with the 2nd edition of Spivey's Z Reference Manual. Access ftp://ftp.comlab.ox.ac.uk/pub/Zforum/fuzz for brief information and an order form. Contact Mike Spivey (email ) for further information. CADiZ is a suite of integrated tools for preparing and type-checking Z specifications as professional quality typeset documents. The Z dialect it recognizes is evolving in line with the standard. The typesetting can be performed by either troff or LaTeX for Unix or Word for Windows. The mouse can be used to interact with a view of the typeset specification to inspect properties deduced by the type-checker, to see the expansion of schema calculus expressions, and to reason about conjectures such as proof obligations. The PC version is integrated with MS Word using OLE2, providing WYSIWYG editing of Z paragraphs directly in Word documents. (The troff and LaTeX versions use ordinary text editors on ASCII mark-up.) Further development of the tools is ongoing. CADiZ is a BCS Award winning product available for Sun, SGI and PC machines from York Software Engineering Ltd, The Innovation Centre, York Science Park, Heslington, York, YO1 5DG, UK (email yse@minster.york.ac.uk, tel +44-1904-435206, fax +44-1904-435135). ProofPower is a suite of tools supporting specification and proof in Higher Order Logic (HOL) and in Z. Short courses on ProofPower-Z are available as demand arises. Information about ProofPower can be obtained automatically by sending email to . Contact Roger Jones, International Computers Ltd, Eskdale Road, Winnersh, Wokingham, Berkshire RG11 5TT, UK (tel +44-118-969-3131 ext 6536, fax +44-118-969-7636, email ) for further details. Zola is a commercial integrated support tool for Z on Sun workstations, for automated assistance at all stages of the specification construction, proving and maintenance process. It is intended for system developers and includes a WYSIWYG editor, type-checker and tactical theorem prover suitable for the creation and maintenance of large specifications. For further information, contact Chris Paine or Will Harwood, Imperial Software Technology, 62-74 Burleigh Street, Cambridge CB1 1DJ, UK (tel +44-1223-462400, fax +44-1223-462500, email ). ZTC is a Z type-checker available free of charge for educational and non-profit uses. It is intended to be compliant with the 2nd edition of Spivey's Z Reference Manual. It accepts LaTeX with "zed" or "oz" styles, and ZSL - an ASCII version of Z. ZANS is a Z animator. It is a research prototype that is still very crude. Both ZTC and ZANS run on Linux, SunOS 4.x, Solaris 2.x, HP-UX 9.0, DOS, and extended DOS. They are available via anonymous FTP under ftp://ise.cs.depaul.edu/pub in the directories ZANS-x.xx and ZTC-x.xx, where x.xx are version numbers. Contact Xiaoping Jia for further information. Formaliser is a syntax-directed WYSIWYG Z editor and interactive type checker, running under Microsoft Windows, available from Logica. Contact Susan Stepney, Logica UK Limited, Cambridge Division, Betjeman House, 104 Hills Road, Cambridge CB2 1LQ, UK (tel +44-1223-366343, fax +44-1223-251001, email ) or see under http://public.logica.com/~formaliser/formlsr/formlsr.htm on-line. DST-fuzz is a set of tools based on the fuzz package by Mike Spivey, supplying a Motif based user interface for LaTeX based pretty printing, syntax and type-checking. A CASE tool interface allows basic functionality for combined application of Z together with structured specifications. The tools are integrated into SoftBench. For further information contact Hans-Martin Hoercher, DST Deutsche System-Techik GmbH, Edisonstr. 3, D-24145 Kiel, Germany (tel +49-431-7109-478, fax +49-431-7109-503, email ). The B-Tool can be used to check proofs concerning parts of Z specifications. This is licensed by Edinburgh Portable Compilers Ltd, 17 Alva Street, Edinburgh EH2 4PH, UK (tel +44-131-225-6262, fax +44-131-225-6644). Contact the Distribution Manager (email ) for further information. The B-Toolkit is a set of integrated tools which fully supports the B-Method for formal software development and is available from B-Core (UK) Limited, Magdalen Centre, The Oxford Science Park, Oxford OX4 4GA, UK. For further details, contact Ib Sorensen (tel +44-1865-784520, fax +44-1865-784518, email ) or see http://www-scm.tees.ac.uk/bresource/docs/B/btoolkit.html on-line. Z fonts for MS Windows and Macintosh are available on-line. For hyperlinks to these and other Z tool resources see the WWW Z page: http://www.comlab.ox.ac.uk/archive/z.html#tools A survey of Z tools (produced in 1991) may be obtained from Colin Parker, Systems Process Department, W376C, British Aerospace, Warton Aerodrome, Warton, Preston PR4 1AX, UK. | Nitpick is a freely available tool for fully automatically analyzing |software specifications in (roughly) a subset of Z. See |http://www.cs.cmu.edu/~nitpick/ Subject: How can I learn about Z? There are a number of courses on Z run by industry and academia. Oxford University offers industrial short courses in the use Z. As well as introductory courses, recent newly developed material includes advanced Z-based courses on proof and refinement, partly based around the B-Tool. Courses are held in Oxford, or elsewhere (e.g., on a company's premises) if there is enough demand. For further information, contact Jim Woodcock (tel +44-1865-283514, fax +44-1865-273839, email ). Logica offer a five day course on Z at company sites. Contact Rosalind Barden (tel +44-1223-366343 ext 4860, fax +44-1223-322315, email ) at Logica UK Limited, Betjeman House, 104 Hills Road, Cambridge CB2 1LQ, UK. Praxis Systems plc runs a range of Z (and other formal methods) courses. For details contact Anthony Hall on +44-1225-444700 or . Formal Systems (Europe) Ltd run a range of Z, CSP and other formal methods courses, primarily in the US and with such lecturers as Jim Woodcock and Bill Roscoe (both lecturers at the OUCL). For dates and prices contact Kate Pearson (tel +44-1865-728460, fax +44-1865-201114) at Formal Systems (Europe) Limited, 3 Alfred Street, Oxford OX1 4EH, UK. DST Deutsche System-Technik runs a collection of courses for either Z or CSP, mainly in Germany. These courses range from half day introductions to formal methods and Z to one week introductory or advanced courses, held either at DST, or elsewhere. For further information contact Hans-Martin Hoercher, DST Deutsche System-Techik GmbH, Edisonstr. 3, D-24145 Kiel, Germany (tel +49-431-7109-478, fax +49-431-7109-503, email ). Subject: What has been published about Z? A searchable on-line Z bibliography is available on the World Wide Web under http://www.comlab.ox.ac.uk/archive/z/bib.html in BibTeX format. For those without WWW access, an older compressed version is available under ftp://ftp.comlab.ox.ac.uk/pub/Zforum/z.bib.Z (and also ftp://ftp.comlab.ox.ac.uk/pub/Zforum/z.ps.Z in PostScript format). Information on OUCL Technical Monographs and Reports, including many on Z, is available from the librarian (tel +44-1865-273837, fax +44-1865-273839, email ). "Formal Methods: A Survey" by S.Austin & G.I.Parkin, March 1993 includes information on the use and teaching of Z in industry and academia. Contact DITC Office, Formal Methods Survey, National Laboratory, Teddington, Middlesex TW11 0LW, UK (tel +44-181-943-7002, fax +44-181-977-7091) for a copy. The following books largely concerning Z have been or are due to be published (in approximate chronological order): I.Hayes (ed.), Specification Case Studies, Prentice Hall International Series in Computer Science, 1987. (2nd ed., 1993) URL: http://www.prenhall.com/013/832543/ptr/83254-3.html J.M.Spivey, Understanding Z: A specification language and its formal semantics, Cambridge University Press, 1988. D.Ince, An Introduction to Discrete Mathematics, Formal System Specification and Z, Oxford University Press, 1988. (2nd ed., 1993) J.C.P.Woodcock & M.Loomes, Software Engineering Mathematics: Formal Methods Demystified, Pitman, 1998. (Also Addision-Wesley, 1989) J.M.Spivey, The Z Notation: A reference manual, Prentice Hall International Series in Computer Science, 1989. (2nd ed., 1992) [Widely used as a de facto standard for Z. Often known as ZRM2.] A.Diller, Z: An introduction to formal methods, Wiley, 1990. J.E.Nicholls (ed.), Z user workshop, Oxford 1989, Springer-Verlag, Workshops in Computing, 1990. B.Potter, J.Sinclair & D.Till, An Introduction to Formal Specification and Z, Prentice Hall International Series in Computer Science, 1991. | (2nd ed., 1996) URL: http://www.prenhall.com/013/242206/ptr/24220-6.html D.Lightfoot, Formal Specification using Z, MacMillan, 1991. A.Norcliffe & G.Slater, Mathematics for Software Construction, Ellis Horwood, 1991. J.E.Nicholls (ed.), Z User Workshop, Oxford 1990, Springer-Verlag, Workshops in Computing, 1991. I.Craig, The Formal Specification of Advanced AI Architectures, Ellis Horwood, 1991. M.Imperato, An Introduction to Z, Chartwell-Bratt, 1991. J.B.Wordsworth, Software Development with Z, Addison-Wesley, 1992. S.Stepney, R.Barden & D.Cooper (eds.), Object Orientation in Z, Springer-Verlag, Workshops in Computing, August 1992. URL: http://public.logica.com/~stepneys/bib/ss/ooz.htm J.E.Nicholls (ed.), Z User Workshop, York 1991, Springer-Verlag, Workshops in Computing, 1992. URL: http://www.imi.gla.ac.uk/springer/eWiC/Abstracts/9.html D.Edmond, Information Modeling: Specification and implementation, Prentice Hall, 1992. J.P.Bowen & J.E.Nicholls (eds.), Z User Workshop, London 1992, Springer-Verlag, Workshops in Computing, 1993. URL: http://www.comlab.ox.ac.uk/archive/z/zum92.html S.Stepney, High Integrity Compilation: A case study, Prentice Hall, 1993. URL: http://public.logica.com/~stepneys/bib/ss/hic.htm M.McMorran & S.Powell, Z Guide for Beginners, Blackwell Scientific, 1993. K.C.Lano & H.Haughton (eds.), Object-oriented Specification Case Studies, Prentice Hall International Object-Oriented Series, 1993. B.Ratcliff, Introducing Specification using Z: A practical case study approach, McGraw-Hill, 1994. A.Diller, Z: An introduction to formal methods, 2nd ed., Wiley, 1994. J.P.Bowen & J.A.Hall (eds.), Z User Workshop, Cambridge 1994, Springer-Verlag, Workshops in Computing, 1994. URL: http://www.comlab.ox.ac.uk/archive/z/zum94.html R.Barden, S.Stepney & D.Cooper, Z in Practice, Prentice Hall BCS Practitioner Series, 1994. URL: http://public.logica.com/~stepneys/bib/ss/zip.htm D.Rann, J.Turner & J.Whitworth, Z: A beginner's guide. Chapman & Hall, 1994. D.Heath, D.Allum & L.Dunckley, Introductory Logic and Formal Methods. A.Waller, Henley-on-Thames, 1994. L.Bottaci and J.Jones, Formal Specification using Z: A modelling approach. International Thomson Publishing, 1995. D.Sheppard, An Introduction to Formal Specification with Z and VDM. McGraw Hill International Series in Software Engineering, 1995. J.P.Bowen & M.G.Hinchey (eds.), ZUM'95: The Z Formal Specification Notation, Springer-Verlag, Lecture Notes in Computer Science, volume 967, 1995. URL: http://www.comlab.ox.ac.uk/archive/z/zum95.html J.P.Bowen, Formal Specification and Documentation using Z: A Case Study Approach, International Thomson Compress Press, 1996. URL: http://www.comlab.ox.ac.uk/oucl/users/jonathan.bowen/zbook.html J.C.P.Woodcock & J.Davies, Using Z: Specification, proof and refinement, Prentice Hall International Series in Computer Science, 1996. URL: http://www.comlab.ox.ac.uk/usingz.html A.Harry, Formal Methods Fact File: VDM and Z, Wiley, 1996. Announced: J.Jacky, The Way of Z: Formal Methods Demystified, Cambridge University Press, November 1996. L.Semmens, Z for Software Engineers, Ellis Horwood Series in Computers and Their Applications, December 1996. See also an on-line list of Z books from Blackwells Bookshop under: http://www.blackwell.co.uk/cgi-bin/bb_catsel?09_IBY Subject: What is object-oriented Z? Several object-oriented extensions to or versions of Z have been proposed. The book "Object orientation in Z", listed above, is a collection of papers describing various OOZ approaches - Hall, ZERO, MooZ, Object-Z, OOZE, Schuman&Pitt, Z++, ZEST and Fresco (an OO VDM method) - in the main written by the methods' inventors, and all specifying the same two examples. A more recent book entitled "Object-oriented specification case studies" surveys the principal methods and languages for formal object-oriented specification, including Z-based approaches. Subject: How can I run Z? Z is a (non-executable in general) specification language, so there is no such thing as a Z compiler/linker/etc. as you would expect for a programming language. Some people have looked at animating subsets of Z for rapid prototyping purposes, using logic and functional programming for example, but this work is preliminary and is not really the major point of Z, which is to increase human understandability of the specified system and allow the possibility of formal reasoning and development. However, Prolog seems to be the main favoured language for Z prototyping and some references may be found in the Z bibliography (see above). Subject: Where can I meet other Z people? The 10th International Conference of Z Users (ZUM'97) will be held 3-4 April 1997 at the University of Reading, UK. For general enquiries, contact the Conference Chair, Jonathan Bowen (tel +44-118-931-6544, fax +44-118-975-1994, email ). Information on ZUM'97 is available under http://www.cs.reading.ac.uk/archive/z/zum97/ via WWW. Information on Z User Meetings is issued on newsgroups including comp.specification.z, the Z postal mailing list and various specialist electronic mailing lists. The 9th International Conference of Z Users (ZUM'95) was held 7-9 September 1995 in Limerick, Ireland. The proceedings appeared in the Springer-Verlag LNCS series (volume 967). Previous proceedings for Z User Meetings have been published in the Springer-Verlag Workshops in Computing series since the 4th meeting in 1989. See the URL http://www.comlab.ox.ac.uk/archive/z/zum.html for further on-line information on previous meetings. For a list of meetings with a formal methods content, see: http://www.comlab.ox.ac.uk/archive/formal-methods/meetings.html Subject: What is the Z User Group? The Z User Group was set up in 1992 to oversee Z-related activities, and the Z User Meetings in particular. As a subscriber to either comp.specification.z, ZFORUM or the postal mailing list, you may consider yourself a member of the Z User Group. There are currently no charges for membership, although this is subject to review if necessary. Contact for further information. Subject: How can I obtain the draft Z standard? The proposed Z standard under ISO/IEC JTC1/SC22 is available electronically via anonymous FTP *only* (not via the mail server since it is too large) from the Z archive at Oxford in compressed PostScript format. Version 1.0 of the draft standard is accessible as the file ftp://ftp.comlab.ox.ac.uk/pub/Zforum/zstandard1.0.ps.Z together with an annex in ftp://ftp.comlab.ox.ac.uk/pub/Zforum/zstandard-annex1.0.ps.Z It is also available in printed form from the OUCL librarian (tel +44-1865-273837, fax +44-1865-273839, email ) by requesting Technical Monograph number PRG-107. Subject: Where else is Z discussed? The BCS-FACS (British Computer Society Formal Aspects of Computer Science special interest group) and FME (Formal Methods Europe) are two organizations interested in formal methods in general. Contact BCS FACS, Dept of Computer Studies, Loughborough University of Technology, Loughborough, Leicester LE11 3TU, UK (tel +44-1509-222676, fax +44-1509-211586, email ) for further information. A "FACS Europe" newsletter is issued to members of FACS and FME. Please send suitable Z-related material to the Z column editor, David Till, Dept of Computer Science, City University, Northampton Square, London, EC1V 0HB, UK (tel +44-171-477-8552, email ) for possible publication. Material from articles appearing on the comp.specification.z newsgroup may be included if considered of sufficient interest (with permission from the originator if possible). It would be helpful for posters of articles on comp.specification.z to indicate if they do not want further distribution for any reason. Subject: How does VDM compare with Z? See I.J.Hayes, C.B.Jones & J.E.Nicholls, Understanding the differences between VDM and Z, FACS Europe, series I, 1(1):7-30, Autumn 1993 available as an on-line Technical Report from Manchester under ftp://ftp.cs.man.ac.uk/pub/TR/UMCS-93-8-1.ps.Z and I.J.Hayes, VDM and Z: A comparative case study, Formal Aspects of Computing, 4(1):76-99, 1992. VDM is discussed on the (unmoderated) VDM FORUM mailing list. Send a message containing the command "join vdm-forum " where is your real name to . To contact the list administrator, email John Fitzgerald on . Subject: How does the B-Method compare with Z? See http://www.b-core.com/ZVdmB.html for a comparison. See also http://www.comlab.ox.ac.uk/archive/formal-methods/b.html for further information on B. Subject: What if I have spotted a mistake or an omission? Please send corrections or new relevant information about meetings, books, tools, etc., to . New questions and model answers are also gratefully received! -- Jonathan Bowen Department of Computer Science, University of Reading, UK URL: http://www.cs.reading.ac.uk/people/jpb/ From csus.edu!csulb.edu!gatech!news-out.communique.net!communique!news3.epix.net!news.sprintlink.net!news-pen-14.sprintlink.net!www.nntp.primenet.com!nntp.primenet.com!rill.news.pipex.net!pipex!warwick!lyra.csx.cam.ac.uk!news.ox.ac.uk!zforum-request Wed Apr 2 11:03:41 1997 Path: csus.edu!csulb.edu!gatech!news-out.communique.net!communique!news3.epix.net!news.sprintlink.net!news-pen-14.sprintlink.net!www.nntp.primenet.com!nntp.primenet.com!rill.news.pipex.net!pipex!warwick!lyra.csx.cam.ac.uk!news.ox.ac.uk!zforum-request From: zforum-request@comlab.ox.ac.uk Newsgroups: comp.specification.z,comp.specification.misc,comp.answers,news.answers Subject: comp.specification.z Frequently Asked Questions (Monthly) Supersedes: Followup-To: comp.specification.z Date: Tue, 1 Apr 1997 01:00:06 GMT Organization: Z User Group Lines: 429 Sender: news@comlab.ox.ac.uk (News) Approved: news-answers-request@MIT.Edu Expires: Tue, 13 May 1997 01:00:01 GMT Message-ID: Reply-To: J.P.Bowen@reading.ac.uk NNTP-Posting-Host: gruffle.comlab.ox.ac.uk Summary: Information about the Z formal specification notation Originator: news@gruffle.comlab Xref: csus.edu comp.specification.z:2803 comp.specification.misc:969 comp.answers:25306 news.answers:99406 Archive-name: z-faq Last-modified: 6 February 1997 Maintainer: Jonathan Bowen URL: ftp://ftp.comlab.ox.ac.uk/pub/Zforum/faq NAME: comp.specification.z STATUS: unmoderated PURPOSE: Discussion concerning the formal specification notation Z. (If you have read this before, changed and new sections since the previously issued version are marked with `|' in the left hand margin.) Questions have been marked with "Subject:" at the start of the line to allow some newsreaders to scan them easily (e.g., "^G" within "rn"). Subject: What is it? Z (pronounced `zed') is a formal specification notation based on set theory and first order predicate logic. It has been developed at the Programming Research Group at the Oxford University Computing Laboratory (OUCL) and elsewhere since the late 1970s. It is used by industry as part of the software (and hardware) development process in Europe, USA and elsewhere. Currently it is undergoing international ISO standardization. The comp.specification.z electronic USENET newsgroup was established in June 1991 and is intended to handle messages concerned with Z. It has an estimated readership of tens of thousands of people worldwide. Comp.specification.z provides a convenient forum for messages concerned with recent developments and the use of Z. Pointers to and reviews of recent books and articles are particularly encouraged. These may be included in the Z bibliography (see below) if they appear in comp.specification.z. Subject: What if I do not have access to USENET news? There is an associated Z FORUM electronic mailing list that was initiated in January 1986 by Ruaridh Macdonald, RSRE, UK. Articles are now automatically cross-posted between comp.specification.z and the mailing list for those whose do not have access to USENET news. This may apply especially to industrial Z users who are particularly encouraged to subscribe and post their experiences to the list. Please contact with your name, address and email address to join the mailing list (or if you change your email address or wish to be removed from the list). Readers are strongly urged to read the comp.specification.z newsgroup rather than the Z FORUM mailing list if possible. Messages for submission to the Z FORUM mailing list and the comp.specification.z newsgroup may be emailed to . This method of posting is particularly recommended for important messages like announcements of meetings since not all messages posted on comp.specification.z reach the OUCL. A mailing list for the Z User Meeting educational issues session has been set by Neville Dean, Anglia Polytechnic University, UK. Anyone interested may join by emailing with your contact details. A specialist electronic mailing for discussion of SAZ, a combination of the structured method SSADM and Z existed for a while, but is now closed. Subject: What if I do not have access to email? If you wish to join the postal Z mailing list, please send your address to Amanda Kingscote, Praxis plc, 20 Manvers Street, Bath BA1 1PX, UK (tel +44-1225-444700, fax +44-1225-465205, email ). This will ensure you receive details of Z meetings, etc., particularly for people without access to electronic mail. Subject: How can I join in? If you are currently using Z, you are welcome to introduce yourself to the newsgroup and Z FORUM list by describing your work with Z or raising any questions you might have about Z which are not answered here. You may also advertize publications concerning Z which you or your colleagues produce. These may then be added to the master Z bibliography maintained at the OUCL (see below). Subject: Where are Z-related files archived? Information on the World Wide Web (WWW) is available under the http://www.comlab.ox.ac.uk/archive/z.html page. See also the http://www.comlab.ox.ac.uk/archive/formal-methods.html page on formal methods in general. The WWW global hypermedia system is accessible using the "netscape", "mosaic" or "lynx" programs for example. Contact your system manager if WWW access is not available on your system. Some of the Z archive is also available via anonymous FTP under ftp://ftp.comlab.ox.ac.uk/pub/Zforum (IP address 163.1.27.2 if you have access problems). The README file provides some general information and 00index gives a list of the files. If you cannot access the Internet directly, there is an automatic electronic mail-based electronic archive server which allows access to some of the Z FTP archive. Send an email message containing the command "help" to for further information on how to use the server. If you have serious trouble accessing the archive server, please contact the address . Subject: What tools are available? Various tools for formatting, type-checking and aiding proofs in Z are available. A free LaTeX style file and documentation can be obtained from the OUCL archive. Access the ftp://ftp.comlab.ox.ac.uk/pub/Zforum/zed.sty and ftp://ftp.comlab.ox.ac.uk/pub/Zforum/zguide.tex files. A newer style "csp_zed.sty" is available in the same location, which uses the new font selection scheme and covers CSP and Z symbols. A style for Object-Z "oz.sty" with a guide "oz.tex" is also accessible. LaTeX2e users may find "zed-csp.sty" and "zed2e.tex" useful. The fuzz package, a syntax and type-checker with a LaTeX style option and fonts, is available from the Spivey Partnership, 10 Warneford Road, Oxford OX4 1LU, UK. It is compatible with the 2nd edition of Spivey's Z Reference Manual. Access ftp://ftp.comlab.ox.ac.uk/pub/Zforum/fuzz for brief information and an order form. Contact Mike Spivey (email ) for further information. CADiZ is a suite of integrated tools for preparing and type-checking Z specifications as professional quality typeset documents. The Z dialect it recognizes is evolving in line with the standard. The typesetting can be performed by either troff or LaTeX for Unix or Word for Windows. The mouse can be used to interact with a view of the typeset specification to inspect properties deduced by the type-checker, to see the expansion of schema calculus expressions, and to reason about conjectures such as proof obligations. The PC version is integrated with MS Word using OLE2, providing WYSIWYG editing of Z paragraphs directly in Word documents. (The troff and LaTeX versions use ordinary text editors on ASCII mark-up.) Further development of the tools is ongoing. CADiZ is a BCS Award winning product available for Sun, SGI and PC machines from York Software Engineering Ltd, The Innovation Centre, York Science Park, Heslington, York, YO1 5DG, UK (email yse@minster.york.ac.uk, tel +44-1904-435206, fax +44-1904-435135). ProofPower is a suite of tools supporting specification and proof in Higher Order Logic (HOL) and in Z. Short courses on ProofPower-Z are available as demand arises. Information about ProofPower can be obtained automatically by sending email to . Contact Roger Jones, International Computers Ltd, Eskdale Road, Winnersh, Wokingham, Berkshire RG11 5TT, UK (tel +44-118-969-3131 ext 6536, fax +44-118-969-7636, email ) for further details, or see: http://www.trireme.demon.co.uk/ Zola is a commercial integrated support tool for Z on Sun workstations, for automated assistance at all stages of the specification construction, proving and maintenance process. It is intended for system developers and includes a WYSIWYG editor, type-checker and tactical theorem prover suitable for the creation and maintenance of large specifications. For further information, contact Chris Paine, Imperial Software Technology Ltd, Berkshire House, 252 Kings Road, Reading RG1 4HP, UK (tel +44-118-958-7055, fax +44-118-958-9005, email ), or see: http://www.ist.co.uk/products/zola.html ZTC is a Z type-checker available free of charge for educational and non-profit uses. It is intended to be compliant with the 2nd edition of Spivey's Z Reference Manual. It accepts LaTeX with "zed" or "oz" styles, and ZSL - an ASCII version of Z. ZANS is a Z animator. It is a research prototype that is still very crude. Both ZTC and ZANS run on Linux, SunOS 4.x, Solaris 2.x, HP-UX 9.0, DOS, and extended DOS. They are available via anonymous FTP under ftp://ise.cs.depaul.edu/pub in the directories ZANS-x.xx and ZTC-x.xx, where x.xx are version numbers. Contact Xiaoping Jia for further information. Formaliser is a syntax-directed WYSIWYG Z editor and interactive type checker, running under Microsoft Windows, available from Logica. Contact Susan Stepney, Logica UK Limited, Cambridge Division, Betjeman House, 104 Hills Road, Cambridge CB2 1LQ, UK (tel +44-1223-366343, fax +44-1223-251001, email ) or see under http://public.logica.com/~formaliser/formlsr/formlsr.htm on-line. DST-fuzz is a set of tools based on the fuzz package by Mike Spivey, supplying a Motif based user interface for LaTeX based pretty printing, syntax and type-checking. A CASE tool interface allows basic functionality for combined application of Z together with structured specifications. The tools are integrated into SoftBench. For further information contact Hans-Martin Hoercher, DST Deutsche System-Techik GmbH, Edisonstr. 3, D-24145 Kiel, Germany (tel +49-431-7109-478, fax +49-431-7109-503, email ). The B-Toolkit is a set of integrated tools which fully supports the B-Method for formal software development and is available from B-Core (UK) Limited, Magdalen Centre, The Oxford Science Park, Oxford OX4 4GA, UK. For further details, contact Ib Sorensen (tel +44-1865-784520, fax +44-1865-784518, email ) or see http://www.b-core.com/ on-line. Nitpick is a freely available tool for fully automatically analyzing software specifications in (roughly) a subset of Z. See http://www.cs.cmu.edu/~nitpick/ Z/EVES is an analysis tool for Z specifications, that can be used to check for syntax, type-correctness and "domain errors" (are functions applied on their domain?), expand schemas, calculate preconditions and check for totality, and state and prove conjectures, with the aid of a heuristic theorem prover. It supports the "zed"/"fuzz" style LaTeX markup. and runs on SunOS, OS/2, Linux, Windows 3.1, Windows'95 and, with the appropriate compatibility package from Sun, Solaris. It is available electronically at no cost. Email eves@ora.on.ca or see: http://www.ora.on.ca/distribution.html Z fonts for MS Windows and Macintosh are available on-line. For hyperlinks to these and other Z tool resources see the WWW Z page: http://www.comlab.ox.ac.uk/archive/z.html#tools Subject: How can I learn about Z? There are a number of courses on Z run by industry and academia. Oxford University offers industrial short courses in the use Z. As well as introductory courses, recent newly developed material includes advanced Z-based courses on proof and refinement, partly based around the B-Tool. Courses are held in Oxford, or elsewhere (e.g., on a company's premises) if there is enough demand. For further information, contact Jim Woodcock (tel +44-1865-283514, fax +44-1865-273839, email ). Logica offer a five day course on Z at company sites. Contact Rosalind Barden (tel +44-1223-366343 ext 4860, fax +44-1223-322315, email ) at Logica UK Limited, Betjeman House, 104 Hills Road, Cambridge CB2 1LQ, UK. Praxis Systems plc runs a range of Z (and other formal methods) courses. For details contact Anthony Hall on +44-1225-444700 or . Formal Systems (Europe) Ltd run a range of Z, CSP and other formal methods courses, primarily in the US and with such lecturers as Jim Woodcock and Bill Roscoe (both lecturers at the OUCL). For dates and prices contact Kate Pearson (tel +44-1865-728460, fax +44-1865-201114) at Formal Systems (Europe) Limited, 3 Alfred Street, Oxford OX1 4EH, UK. DST Deutsche System-Technik runs a collection of courses for either Z or CSP, mainly in Germany. These courses range from half day introductions to formal methods and Z to one week introductory or advanced courses, held either at DST, or elsewhere. For further information contact Hans-Martin Hoercher, DST Deutsche System-Techik GmbH, Edisonstr. 3, D-24145 Kiel, Germany (tel +49-431-7109-478, fax +49-431-7109-503, email ). Subject: What has been published about Z? A searchable on-line Z bibliography is available on the World Wide Web under http://www.comlab.ox.ac.uk/archive/z/bib.html in BibTeX format. The following books largely concerning Z have been or are due to be published (in approximate chronological order): I.Hayes (ed.), Specification Case Studies, Prentice Hall International Series in Computer Science, 1987. (2nd ed., 1993) URL: http://www.prenhall.com/013/832543/ptr/83254-3.html J.M.Spivey, Understanding Z: A specification language and its formal semantics, Cambridge University Press, 1988. D.Ince, An Introduction to Discrete Mathematics, Formal System Specification and Z, Oxford University Press, 1988. (2nd ed., 1993) J.C.P.Woodcock & M.Loomes, Software Engineering Mathematics: Formal Methods Demystified, Pitman, 1998. (Also Addision-Wesley, 1989) J.M.Spivey, The Z Notation: A reference manual, Prentice Hall International Series in Computer Science, 1989. (2nd ed., 1992) [Widely used as a de facto standard for Z. Often known as ZRM2.] A.Diller, Z: An introduction to formal methods, Wiley, 1990. J.E.Nicholls (ed.), Z user workshop, Oxford 1989, Springer-Verlag, Workshops in Computing, 1990. B.Potter, J.Sinclair & D.Till, An Introduction to Formal Specification and Z, Prentice Hall International Series in Computer Science, 1991. (2nd ed., 1996) URL: http://www.prenhall.com/013/242206/ptr/24220-6.html D.Lightfoot, Formal Specification using Z, MacMillan, 1991. A.Norcliffe & G.Slater, Mathematics for Software Construction, Ellis Horwood, 1991. J.E.Nicholls (ed.), Z User Workshop, Oxford 1990, Springer-Verlag, Workshops in Computing, 1991. I.Craig, The Formal Specification of Advanced AI Architectures, Ellis Horwood, 1991. M.Imperato, An Introduction to Z, Chartwell-Bratt, 1991. J.B.Wordsworth, Software Development with Z, Addison-Wesley, 1992. URL: http://www.aw.com/cseng/authors/wordsworth/softdev/ S.Stepney, R.Barden & D.Cooper (eds.), Object Orientation in Z, Springer-Verlag, Workshops in Computing, August 1992. URL: http://public.logica.com/~stepneys/bib/ss/ooz.htm J.E.Nicholls (ed.), Z User Workshop, York 1991, Springer-Verlag, Workshops in Computing, 1992. URL: http://www.imi.gla.ac.uk/springer/eWiC/Abstracts/9.html D.Edmond, Information Modeling: Specification and implementation, Prentice Hall, 1992. J.P.Bowen & J.E.Nicholls (eds.), Z User Workshop, London 1992, Springer-Verlag, Workshops in Computing, 1993. URL: http://www.comlab.ox.ac.uk/archive/z/zum92.html S.Stepney, High Integrity Compilation: A case study, Prentice Hall, 1993. URL: http://public.logica.com/~stepneys/bib/ss/hic.htm M.McMorran & S.Powell, Z Guide for Beginners, Blackwell Scientific, 1993. K.C.Lano & H.Haughton (eds.), Object-oriented Specification Case Studies, Prentice Hall International Object-Oriented Series, 1993. B.Ratcliff, Introducing Specification using Z: A practical case study approach, McGraw-Hill, 1994. A.Diller, Z: An introduction to formal methods, 2nd ed., Wiley, 1994. J.P.Bowen & J.A.Hall (eds.), Z User Workshop, Cambridge 1994, Springer-Verlag, Workshops in Computing, 1994. URL: http://www.comlab.ox.ac.uk/archive/z/zum94.html R.Barden, S.Stepney & D.Cooper, Z in Practice, Prentice Hall BCS Practitioner Series, 1994. URL: http://public.logica.com/~stepneys/bib/ss/zip.htm D.Rann, J.Turner & J.Whitworth, Z: A beginner's guide. Chapman & Hall, 1994. D.Heath, D.Allum & L.Dunckley, Introductory Logic and Formal Methods. A.Waller, Henley-on-Thames, 1994. L.Bottaci and J.Jones, Formal Specification using Z: A modelling approach. International Thomson Publishing, 1995. D.Sheppard, An Introduction to Formal Specification with Z and VDM. McGraw Hill International Series in Software Engineering, 1995. J.P.Bowen & M.G.Hinchey (eds.), ZUM'95: The Z Formal Specification Notation, Springer-Verlag, Lecture Notes in Computer Science, volume 967, 1995. URL: http://www.comlab.ox.ac.uk/archive/z/zum95.html J.P.Bowen, Formal Specification and Documentation using Z: A Case Study Approach, International Thomson Compress Press, 1996. URL: http://www.comlab.ox.ac.uk/oucl/users/jonathan.bowen/zbook.html J.C.P.Woodcock & J.Davies, Using Z: Specification, proof and refinement, Prentice Hall International Series in Computer Science, 1996. URL: http://www.comlab.ox.ac.uk/usingz.html A.Harry, Formal Methods Fact File: VDM and Z, Wiley, 1996. J.Jacky, The Way of Z: Practical Programming with Formal Methods, Cambridge University Press, 1997. URL: http://www.radonc.washington.edu/prostaff/jon/z-book/ Announced: L.Semmens, Z for Software Engineers, Ellis Horwood Series in Computers and Their Applications, December 1996. J.P.Bowen, M.G.Hinchey & D.Till (eds.), ZUM'97: The Z Formal Specification Notation, Springer-Verlag, Lecture Notes in Computer Science, 1997. URL: http://www.cs.reading.ac.uk/zum97/ See also an on-line list of Z books from Blackwells Bookshop under: http://www.blackwell.co.uk/cgi-bin/bb_catsel?09_IBY "Formal Methods: A Survey" by S.Austin & G.I.Parkin, March 1993 includes information on the use and teaching of Z in industry and academia. Contact DITC Office, Formal Methods Survey, National Laboratory, Teddington, Middlesex TW11 0LW, UK (tel +44-181-943-7002, fax +44-181-977-7091) for a copy. OUCL Technical Monographs and Reports, including many on Z, is available from the OUCL librarian (tel +44-1865-273837, fax +44-1865-273839, email ). For information on formal methods publications in general, see: http://www.comlab.ox.ac.uk/archive/formal-methods/pubs.html Subject: What is object-oriented Z? Several object-oriented extensions to or versions of Z have been proposed. The book "Object orientation in Z", listed above, is a collection of papers describing various OOZ approaches - Hall, ZERO, MooZ, Object-Z, OOZE, Schuman&Pitt, Z++, ZEST and Fresco (an OO VDM method) - in the main written by the methods' inventors, and all specifying the same two examples. A more recent book entitled "Object-oriented specification case studies" surveys the principal methods and languages for formal object-oriented specification, including Z-based approaches. Subject: How can I run Z? Z is a (non-executable in general) specification language, so there is no such thing as a Z compiler/linker/etc. as you would expect for a programming language. Some people have looked at animating subsets of Z for rapid prototyping purposes, using logic and functional programming for example, but this is not really the major point of Z, which is to increase human understandability of the specified system and allow the possibility of formal reasoning and development. However, Prolog seems to be the main favoured language for Z prototyping and some references may be found in the Z bibliography (see above). Subject: Where can I meet other Z people? The 10th International Conference of Z Users (ZUM'97) will be held 3-4 April 1997 at the University of Reading, UK. For general enquiries, contact the Conference Chair, Jonathan Bowen (tel +44-118-931-6544, fax +44-118-975-1994, email ). Information on ZUM'97 is available under http://www.cs.reading.ac.uk/zum97/ via WWW. Information on Z User Meetings is issued on newsgroups including comp.specification.z, the Z postal mailing list and various specialist electronic mailing lists. The 9th International Conference of Z Users (ZUM'95) was held 7-9 September 1995 in Limerick, Ireland. The proceedings appeared in the Springer-Verlag LNCS series (volume 967). Previous proceedings for Z User Meetings have been published in the Springer-Verlag Workshops in Computing series since the 4th meeting in 1989. See the URL http://www.comlab.ox.ac.uk/archive/z/zum.html for further on-line information on previous meetings. For a list of meetings with a formal methods content, see: http://www.comlab.ox.ac.uk/archive/formal-methods/meetings.html Subject: What is the Z User Group? The Z User Group was set up in 1992 to oversee Z-related activities, and the Z User Meetings in particular. As a subscriber to either comp.specification.z, ZFORUM or the postal mailing list, you may consider yourself a member of the Z User Group. There are currently no charges for membership, although this is subject to review if necessary. Contact for further information. Subject: How can I obtain the draft Z standard? The proposed Z standard under ISO/IEC JTC1/SC22 is available on-line. See under http://www.comlab.ox.ac.uk/oucl/groups/zstandards/ for the latest information and locations. An early version is also available in printed form from the OUCL librarian (tel +44-1865-273837, fax +44-1865-273839, email ) by requesting Technical Monograph number PRG-107. Subject: Where else is Z discussed? The BCS-FACS (British Computer Society Formal Aspects of Computer Science special interest group) and FME (Formal Methods Europe) are two organizations interested in formal methods in general. Contact BCS FACS, Dept of Computer Studies, Loughborough University of Technology, Loughborough, Leicester LE11 3TU, UK (tel +44-1509-222676, fax +44-1509-211586, email ) for further information. A "FACS Europe" newsletter is issued to members of FACS and FME. Please send suitable Z-related material to the Z column editor, David Till, Dept of Computer Science, City University, Northampton Square, London, EC1V 0HB, UK (tel +44-171-477-8552, email ) for possible publication. Material from articles appearing on the comp.specification.z newsgroup may be included if considered of sufficient interest (with permission from the originator if possible). It would be helpful for posters of articles on comp.specification.z to indicate if they do not want further distribution for any reason. Subject: How does VDM compare with Z? See I.J.Hayes, C.B.Jones & J.E.Nicholls, Understanding the differences between VDM and Z, FACS Europe, series I, 1(1):7-30, Autumn 1993 available as an on-line Technical Report from Manchester under ftp://ftp.cs.man.ac.uk/pub/TR/UMCS-93-8-1.ps.Z and I.J.Hayes, VDM and Z: A comparative case study, Formal Aspects of Computing, 4(1):76-99, 1992. VDM is discussed on the (unmoderated) VDM FORUM mailing list. Send a message containing the command "join vdm-forum " where is your real name to . To contact the list administrator, email John Fitzgerald on . Subject: How does the B-Method compare with Z? B is a tool-based formal method for software development, conceived by the originator of Z, Jean-Raymond Abrial, whereas Z is designed mainly for specification. See http://www.b-core.com/ZVdmB.html for a comparison. See also http://www.comlab.ox.ac.uk/archive/formal-methods/b.html for further information on B. Subject: What if I have spotted a mistake or an omission? Please send corrections or new relevant information about meetings, books, tools, etc., to . New questions and model answers are also gratefully received! -- Jonathan Bowen Department of Computer Science, University of Reading, UK URL: http://www.cs.reading.ac.uk/people/jpb/