ftp.pasteur.org/FAQ//ftp-pasteur-org-FAQ.zip/FAQ/z-faq

Internet Message Format | 2008-12-01 | 22KB

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: [e-mail]
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: [e-mail]
Expires: 12 Jan 2009 02:00:01 GMT
Message-ID: <ggvgf1$v00$[e-mail]>
Reply-To: [e-mail]
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: [e-mail]
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: [e-mail]
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 <[e-mail]>
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 <[e-mail]> 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 <[e-mail]>.  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 <[e-mail]> 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 [phone], fax [phone], email
<[e-mail]>).  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 <[e-mail]> 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 [e-mail] 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 <[e-mail]>).
  Praxis High Integrity Systems Ltd have run a range of Z (and other
|formal methods) courses (tel [phone], email
|<[e-mail]>.
  Formal Systems (Europe) Ltd run a range of Z, CSP and other formal
methods courses. Contact Kate Pearson (tel [phone], fax
[phone]) 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 <[e-mail]> 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 <[e-mail]>,
tel [phone], fax [phone]) 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 <[e-mail]>.  New questions and
model answers are also gratefully received!

--
Prof Jonathan P. Bowen <[e-mail]>
London South Bank University, Faculty of BICM
Borough Road, London SE1 0AA, United Kingdom
URL: http://www.jpbowen.com/

--
Prof. Jonathan Bowen  Email: [e-mail]  URL: www.jpbowen.com