home *** CD-ROM | disk | FTP | other *** search
- Path: senator-bedfellow.mit.edu!bloom-beacon.mit.edu!npeer.de.kpn-eurorings.net!npeer-ng2.kpn.DE!fu-berlin.de!feed2.jnfs.ja.net!jnfs.ja.net!feeds.news.ox.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 (FAQ)
- Followup-To: comp.specification.z
- Date: Mon, 1 Dec 2008 02:00:01 +0000 (UTC)
- Organization: Z User Group
- Lines: 390
- Approved: news-answers-request@MIT.Edu
- Expires: 12 Jan 2009 02:00:01 GMT
- Message-ID: <ggvgf1$v00$1@frank-exchange-of-views.oucs.ox.ac.uk>
- Reply-To: bowenjp@lsbu.ac.uk
- NNTP-Posting-Host: merc2.comlab.ox.ac.uk
- X-Trace: frank-exchange-of-views.oucs.ox.ac.uk 1228096801 31744 129.67.151.55 (1 Dec 2008 02:00:01 GMT)
- X-Complaints-To: newsmaster@ox.ac.uk
- NNTP-Posting-Date: Mon, 1 Dec 2008 02:00:01 +0000 (UTC)
- Summary: Information about the Z formal specification notation
- URL: http://vl.zuser.org/
- Originator: bowen@merc2.comlab
- Xref: senator-bedfellow.mit.edu comp.specification.z:7612 comp.specification.misc:2775 comp.answers:66202 news.answers:321259
-
- Archive-name: z-faq
- Posting-Frequency: every month
- Last-modified: 4 January 2006
- Maintainer: Jonathan Bowen <bowenjp@lsbu.ac.uk>
- URL: ftp://ftp.comlab.ox.ac.uk/pub/Zforum/faq
- WWW: http://vl.zuser.org/
-
- 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.)
-
- 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. It has recently undergone international
- ISO standardization.
- The comp.specification.z electronic 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. If you do not have direct news access, you can
- search for comp.specification.z articles on the web using
- Google Groups: http://groups.google.com/groups/comp.specification.z
-
- Subject: What if I do not have access to newsgroups?
-
- There is an associated Z FORUM electronic mailing list that was
- initiated in January 1986 by Ruaridh Macdonald, RSRE, UK. Articles
- are automatically cross-posted between comp.specification.z and the
- mailing list for those whose prefer to receive email.
- Please email <zforum-request@comlab.ox.ac.uk> with "subscribe" in the
- body of the message (not the subject line) to join the list and
- "unsubscribe" in the message to leave 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 <zforum@comlab.ox.ac.uk>. 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 up by Neville Dean, Anglia Polytechnic University, UK. Anyone
- interested may join by emailing <zugeis-request@comlab.ox.ac.uk> with
- your contact details.
-
- Subject: What if I prefer postal mail?
-
- If you wish to join the postal Z mailing list, please send your address
- to Amanda Kingscote, Praxis Critical Systems Ltd, 20 Manvers Street,
- Bath BA1 1PX, UK (tel +44-1225-466991, fax +44-1225-469006, email
- <amanda.kingscote@praxis-cs.co.uk>). This will help ensure you receive
- details of Z meetings, etc.
-
- 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 (see below).
-
- Subject: Where are Z-related files archived?
-
- On-line information relevant to the Z notation may be found as part of
- the World Wide Web (WWW) Virtual Library under the following URL:
- http://vl.zuser.org/
- This includes hyperlinks to many Z-related resources available on-line
- around the world. See also the following Virtual Library page on formal
- methods in general: http://vl.fmnet.info/
- An older Z archive is also available via anonymous FTP under:
- ftp://ftp.comlab.ox.ac.uk/pub/Zforum/
-
- Subject: What tools are available?
-
- Various tools for formatting, type-checking and aiding proofs in Z are
- available under: http://vl.zuser.org/#tools
- This includes links to a number of LaTeX style files which support
- the Z notation. Information on Object-Z LaTeX macros ("oz.sty") may be
- |found under: http://www.itee.uq.edu.au/~smith/latex.html
- The FuZZ package, a syntax and type-checker with a LaTeX style option
- and fonts, is available from: http://spivey.oriel.ox.ac.uk/mike/fuzz
- It is compatible with the 2nd edition of Spivey's Z Reference Manual.
- A Community Z Tools (CZT) initiative is underway to coordinate a set
- |open source Z tools using SourceForge. See: http://czt.sourceforge.net/
- 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 LaTeX and Troff 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
- PC, Sun and SGI machines from the University of York.
- URL: http://www-users.cs.york.ac.uk/~ian/cadiz/
- ProofPower is a suite of tools supporting specification and proof in
- Higher Order Logic (HOL) and in Z. As an option, ProofPower also supports
- verification of SPARK-Ada programs against Z specifications using the
- Compliance Notation designed by DERA. Short courses on ProofPower-Z
- are available as demand arises. Information about ProofPower can be
- obtained from the following location:
- http://www.lemma-one.com/ProofPower/index/
- 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 research
- prototype Z animator. Both ZTC and ZANS run on Linux, SunOS, Solaris,
- HP-UX and DOS. They are available under:
- http://se.cs.depaul.edu/fm/ztc.html http://se.cs.depaul.edu/fm/zans.html
- Contact Xiaoping Jia <jia@cs.depaul.edu> for further information.
- Nitpick is a freely available tool for fully automatically analyzing
- software specifications in (roughly) a subset of Z. See under:
- http://www.cs.cmu.edu/~nitpick/
- 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://vl.zuser.org/#tools
- 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 Windows, Linux, Solaris, SunOS and OS/2. It was
- available electronically at no cost, but ORA ceased distribution on
- 3 June 2005. Email eves@ora.on.ca or see: http://www.ora.on.ca/z-eves/
- 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,
- although it is no longer actively supported. See:
- http://www.ist.co.uk/PRODUCTS/zola.html
- Formaliser is a syntax-directed WYSIWYG Z editor and interactive type
- checker, running under Microsoft Windows, available from Logica.
- URL: http://public.logica.com/~formaliser/
-
- 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 Davies (email <Jim.Davies@comlab.ox.ac.uk>).
- Praxis High Integrity Systems Ltd have run a range of Z (and other
- |formal methods) courses (tel +44-1225-466991, email
- |<info@praxis-his.com>.
- Formal Systems (Europe) Ltd run a range of Z, CSP and other formal
- methods courses. Contact Kate Pearson (tel +44-1865-728460, fax
- +44-1865-201114) at Formal Systems (Europe) Limited, 3 Alfred Street,
- Oxford OX1 4EH, UK.
-
- Subject: What has been published about Z?
-
- A searchable on-line Z bibliography is available in BibTeX format under:
- http://vl.zuser.org/bib.html
- 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)
- 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 Addison-Wesley, 1989)
- J.M.Spivey, The Z Notation: A reference manual, Prentice Hall
- International Series in Computer Science, 1989. (2nd ed., 1992)
- URL: http://spivey.oriel.ox.ac.uk/~mike/zrm/
- [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)
- D.Lightfoot, Formal Specification using Z, MacMillan, 1991.
- (2nd ed., Grassroots series, Palgrave, 2001)
- 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://www-users.cs.york.ac.uk/~susan/bib/ss/ooz/index.htm
- J.E.Nicholls (ed.), Z User Workshop, York 1991, Springer-Verlag,
- Workshops in Computing, 1992.
- D.Edmond, Information Modeling: Specification and implementation,
- Prentice Hall, 1992. URL: http://www.icis.qut.edu.au/~davee/im/
- J.P.Bowen & J.E.Nicholls (eds.), Z User Workshop, London 1992,
- Springer-Verlag, Workshops in Computing, 1993.
- URL: http://www.zuser.org/zum92/
- S.Stepney, High Integrity Compilation: A case study, Prentice Hall, 1993.
- URL: http://www-users.cs.york.ac.uk/~susan/bib/ss/hic/index.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.zuser.org/zum94/
- R.Barden, S.Stepney & D.Cooper, Z in Practice, Prentice Hall
- BCS Practitioner Series, 1994.
- URL: http://www-users.cs.york.ac.uk/~susan/bib/ss/zip/index.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.zuser.org/zum95/
- J.P.Bowen, Formal Specification and Documentation using Z: A Case Study
- Approach, International Thomson Compress Press, 1996.
- URL: http://www.zuser.org/zbook/
- J.C.P.Woodcock & J.Davies, Using Z: Specification, proof and refinement,
- Prentice Hall International Series in Computer Science, 1996.
- URL: http://www.usingz.com/
- 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://staff.washington.edu/~jon/z-book/
- J.P.Bowen, M.G.Hinchey & D.Till (eds.), ZUM'97: The Z Formal Specification
- Notation, Springer-Verlag, Lecture Notes in Computer Science,
- volume 1212, 1997. URL: http://www.zuser.org/zum97/
- J.P.Bowen, A.Fett & M.G.Hinchey (eds.), ZUM'98: The Z Formal Specification
- Notation, Springer-Verlag, Lecture Notes in Computer Science,
- volume 1493, 1998. URL: http://www.zuser.org/zum98/
- E.Currie, The Essence of Z, Prentice Hall Europe, The Essence of
- Computing series, 1999.
- N.Nissanke, Formal Specification: Techniques and Applications,
- Springer-Verlag, 1999.
- G.Smith, The Object-Z Specification Language, Kluwer Academic Publishers,
- Advances in Formal Methods series, 2000.
- URL: http://www.itee.uq.edu.au/~smith/objectz.html
- J.P.Bowen, S.Dunne, A.Galloway & S.King (eds.), ZB2000: Formal Specification
- and Development in Z and B, Springer-Verlag, Lecture Notes in Computer
- Science, volume 1878, 2000.
- URL: http://link.springer.de/link/service/series/0558/tocs/t1878.htm
- R.Duke & G.Rose, Formal Object-Oriented Specification using Object-Z.
- MacMillan, Cornerstones of Computing, 2000.
- J.Derrick & E.A.Boiten, Refinement in Z and Object-Z, Springer, FACIT
- series, 2001. URL: http://www.cs.ukc.ac.uk/people/staff/jd1/books/refine/
- D.Bert, J.P.Bowen, M.Henson & K.Robinson (eds.), ZB2002: Formal Specification
- and Development in Z and B, Springer-Verlag, Lecture Notes in Computer
- Science, volume 2272, 2002.
- URL: http://link.springer.de/link/service/series/0558/tocs/t2272.htm
- ISO/IEC, Information Technology - Z Formal Specification Notation -
- Syntax, Type System and Semantics, ISO/IEC 13568:2002, 2002.
- URL: http://www.iso.ch/iso/en/CatalogueDetailPage.CatalogueDetail?CSNUMBER=21573
- D.Bert, J.P.Bowen, S.King & M.Walden (eds.), ZB2003: Formal Specification
- and Development in Z and B, Springer-Verlag, Lecture Notes in Computer
- Science, volume 2651, 2003.
- URL: http://link.springer.de/link/service/series/0558/tocs/t2651.htm
- H.Treharne, S.King, M.Henson & S.Schneider (eds.), ZB2005: Formal
- Specification and Development in Z and B, Springer-Verlag, Lecture Notes
- in Computer Science, volume 3455, 2005.
- URL: http://link.springer.de/link/service/series/0558/tocs/t3455.htm
- For information on formal methods publications in general, see:
- http://vl.fmnet.info/pubs/
-
- 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.
- The leading object-oriented version of Z is Object-Z. See:
- http://www.itee.uq.edu.au/~smith/objectz.html
-
- 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?
-
- Information on Z User Meetings is issued on comp.specification.z and
- other related newsgroups and various specialist electronic mailing
- lists. Previous proceedings for Z User Meetings have been published in
- the Springer-Verlag LNCS and Workshops in Computing series since the
- 4th meeting in 1989. For further on-line information on previous
- Z User Meetings, see the following URL: http://www.zuser.org/zum/
- | From 2000 to 2005, the Z User Meeting combined with the B conferences
- |to form the International Conference of B and Z Users (ZB). The next
- |Z User Meeting will be ZUM 2006, Comulmbia, MD, USA, April 2006.
- |URL: http://www.zuser.org/zum2006/
- For a general list of meetings with a formal methods content, see:
- http://vl.fmnet.info/meetings/
-
- 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 <zforum-request@comlab.ox.ac.uk> for further
- information. For online information, see the following URL:
- http://www.zuser.org/
-
- Subject: How can I obtain the Z standard?
-
- The Z standard under ISO/IEC JTC1/SC22 was available in draft form
- online. See under http://web.comlab.ox.ac.uk/oucl/groups/zstandards/
- for information. An early version is also available
- in printed form from the OUCL librarian (email <library@comlab.ox.ac.uk>,
- tel +44-1865-273837, fax +44-1865-273839) by requesting Technical
- Monograph number PRG-107. For links to recent on-line information, see:
- http://vl.zuser.org/#standards
- To order the ISO/IEC 13568:2002 Z standard from ISO, see:
- http://www.iso.ch/iso/en/CatalogueDetailPage.CatalogueDetail?CSNUMBER=21573
-
- Subject: Where else is Z discussed?
-
- The BCS-FACS (British Computer Society Formal Aspects of Computing
- Science specialist group) and FME (Formal Methods Europe) are two
- organizations interested in formal methods in general. See:
- http://www.bcs-facs.org and http://www.fmeurope.org/
- A "FACS FACTS" newsletter is issued to members of FACS.
-
- 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 in compressed
- PostScript format under: ftp://ftp.cs.man.ac.uk/pub/TR/UMCS-93-8-1.ps.Z
- See also 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. See:
- http://www.jiscmail.ac.uk/lists/VDM-forum.html
- See also http://www.csr.ncl.ac.uk/vdm/ for further information on VDM.
-
- 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://vl.fmnet.info/b/ 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 <bowenjp@lsbu.ac.uk>. New questions and
- model answers are also gratefully received!
-
- --
- Prof Jonathan P. Bowen <bowenjp@lsbu.ac.uk>
- London South Bank University, Faculty of BICM
- Borough Road, London SE1 0AA, United Kingdom
- URL: http://www.jpbowen.com/
-
- --
- Prof. Jonathan Bowen Email: bowenjp@lsbu.ac.uk URL: www.jpbowen.com
-