Usenet 1994 January/usenetsourcesnewsgroupsinfomagicjanuary1994.iso/answers/z-faq

Text File | 1993-12-02 | 19KB | 352 lines

Newsgroups: comp.specification.z,news.answers,comp.answers
Path: senator-bedfellow.mit.edu!bloom-beacon.mit.edu!nic.hookup.net!europa.eng.gtefsd.com!uunet!pipex!uknet!comlab.ox.ac.uk!zforum-request
From: [e-mail]
Subject: comp.specification.z Frequently Asked Questions (Monthly)
Message-ID: <z-faq_754711204@newsserv>
Followup-To: comp.specification.z
Summary: Information about the Z formal specification notation
Originator: [e-mail]
Supersedes: <z-faq_752119204@newsserv>
Sender: [e-mail]
Reply-To: [e-mail]
Organization: Oxford University Computing Laboratory, UK
Date: Wed, 1 Dec 1993 02:00:09 GMT
Approved: [e-mail]
Expires: Wed, 12 Jan 1994 02:00:04 GMT
Lines: 333
Xref: senator-bedfellow.mit.edu comp.specification.z:1094 news.answers:15227 comp.answers:2857

Archive-name: z-faq
Last-modified: 23 November 1993


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 right 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?

The comp.specification.z USENET newsgroup was established in June 1991
and is intended to handle messages concerned with the formal
specification notation Z (pronounced "zed"). It has an estimated
readership of around 25,000 people worldwide.  Z, based on set theory and
first order predicate logic, has been developed at the Programming
Research Group (PRG) at the Oxford University Computing Laboratory and
elsewhere for well over a decade.  It is now used by industry as part
of the software (and hardware) development process in both the UK and
the US. It is currently undergoing BSI standardization in the UK and
has been accepted for the ISO standardisation process internationally.
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 will 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?

Electronic mailing list: There is an associated Z FORUM 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 <[e-mail]> with your name,
address and e-mail address to join the mailing list (or if you change
your e-mail 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
e-mailed to <[e-mail]>.  This method of posting is
particularly recommended for important messages like announcements of
meetings since not all messages posted on \verb"comp.specification.z"
reach the PRG.

Subject: What if I know someone interested without access to e-mail?

Postal mailing list: If you wish to join the postal Z mailing list,
please send your address to Anthony Hall, Praxis Systems plc,
20 Manvers Street, Bath BA1 1PX, UK.  (tel [phone], fax
[phone]) or on <[e-mail]>.  This will ensure you receive
details of Z meetings, etc., particularly for people without access to
electronic mail.

Subject: What if I know someone interested without access to postal mail?

Be reasonable! :-)

Subject: How can I join in?

Subscribers: 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. You may also advertise any publications concerning Z which you or
your colleagues produce. These will then be automatically added to the
master Z bibliography maintained at the PRG and updated for the regular
Z User Meetings.

Subject: Where are the back issues and other public Z-related files?

Archive: There is an automatic mail-based electronic archive server at
the PRG which contains all the back-issues and messages on Z FORUM and
comp.specification.z, as well as a selection of other Z-related files.
Send an e-mail message containing the command "help" to the address
<[e-mail]> for further information on how to use
the server. A command of "index z" will list the Z-related files.
If you have serious trouble accessing the archive server, please
contact the address <[e-mail]>.

FTP access: The archive is also available via anonymous FTP on the
Internet. 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 e-mail address as the password when prompted. The FTP
command "cd Zforum" will get you into the Z archive directory.  The
file "README" gives some general information and "00index" gives a list
of the files. (Retrieve these using the FTP command "get README", for
example.)

Subject: What tools are available?

Tools: 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 PRG archive server. To receive this via e-mail, send
a message containing the command "send z zed.sty zguide.tex" to the PRG
archive server (see above). A newer style "csp_zed.sty" is also
available in the same location, which uses the new font selection
scheme and covers CSP and Z symbols.
  The fuzz package, a syntax and type checker with a LaTeX style
option and fonts, is available from J. M. Spivey Computing Science
Consultancy, 34, Westlands Grove, Stockton Lane, York YO2 0EF. It is
compatible with the second edition of Spivey's Z Reference Manual (see
below). Contact Mike Spivey <[e-mail]> for further
information, or send the command "send z fuzz" to the PRG
archive server for an order form.
  CADiZ, a suite of tools for checking and typesetting Z specifications
is available from York Software Engineering, University of York, YORK
YO1 5DD, UK (tel [phone], fax [phone]). Support is
available for Unix troff and more recently for LaTeX. Contact David
Jordan at York on <[e-mail]> for further information.
  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. For further information, contact R.B. Jones,
International Computers Ltd, Eskdale Road, Winnersh, Wokingham, BERKS
RG11 5TT, UK (tel [phone] ext 6536, fax [phone], email
<[e-mail]> or <[e-mail]>).
Information about ProofPower can also be obtained directly from
<[e-mail]>.
  Zola is a tool that supports the production and typesetting of Z
specifications, including a type-checker and a Tactical Proof System. The
tool is sold commercially and available to academic users at a special
discount.  For further information, contact K. Ashoo, Imperial
Software Technology, 62-74 Burleigh Street, Cambridge CB1 1DJ, UK (tel
[phone], fax [phone], email <[e-mail]>).
  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 [phone], fax
[phone]). Contact the Distribution Manager on the address
<[e-mail]> for further information.  A Z proof tool called
zedB, which is based on the B-Tool, was presented at the 1991 Z User
Meeting; this may be made available in due course.
  There is a Z tool for PCs which is available from Logica Cambridge.
Contact Roy Maclean, Logica Cambridge Ltd, Betjeman House, 104 Hills
Road, Cambridge CB2 1LQ, UK.
  A survey of Z tools 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?

Courses: 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 zedB 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 [phone], fax
[phone]) on <[e-mail]>.
  Logica Cambridge offer a five day course on Z and a three day
introductory course on formal methods (mainly Z).  For dates and prices
contact Debi Kearney on [phone] ext 4859.
  Praxis Systems runs a range of Z (and other formal methods) courses.
For details contact Anthony Hall on [phone] or <[e-mail]>.
  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 PRG).  For dates and          |
prices contact Joy Reed [phone] email <[e-mail]>       |
(at the PRG) or Kate Pearson [phone] (at Formal Systems).              |


Subject: What has been published about Z?

Publications: A BibTeX bibliography of Z-related publications is
available from the PRG archive server (see above).  Information on
Oxford University Programming Research Group (PRG) Technical Monographs
and Reports, including many on Z, is available from the librarian on
<[e-mail]>.
  "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 [phone],
fax [phone]) 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)
  J.M.Spivey, Understanding Z: a specification language and its formal
      semantics, Cambridge University Press, 1988.
  D.Ince, An introduction to discrete mathematics and formal system
      specification, Oxford University Press, 1988. (2nd ed., 199?)
  J.C.P.Woodcock & M.Loomes, Software engineering mathematics, Pitman, 1988.
  J.M.Spivey, The Z notation: a reference manual, Prentice Hall
      International Series in Computer Science, 1989. (2nd ed., 1992) +
  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.
  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, September 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.
  J.E.Nicholls (ed.), Z user workshop, York 1991, Springer-Verlag,
      Workshops in Computing, 1992.
  J.P.Bowen & J.E.Nicholls (eds.), Z user workshop, London 1992,
      Springer-Verlag, Workshops in Computing, 1993.
  S.Stepney, High integrity compilation: A case study, Prentice Hall, 1993.
  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.               |
Announced:
  J.C.P.Woodcock, Using standard Z, Prentice Hall International Series
      in Computer Science, 1993? (In preparation)
  R.Barden, S.Stepney, D.Cooper, Z in practice (A methods handbook for Z),
      Prentice-Hall, 1994. (In preparation)
  A.Diller, Z: an introduction to formal methods, 2nd ed., Wiley, c1994.
      (Planned)

  + Widely considered as the current de facto standard for Z.

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. "Object-oriented specification case
studies", also listed above, 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?

Meetings: The 7th annual Z User Meeting with an industrial theme was
held on 14-15 December 1992 at the DTI A preprint proceedings and draft
Z standard were distributed to delegates. A published proceedings is in
press; ordering details are available from the Z archive (see above) in
the file "zum92". An 8th meeting (ZUM'94) is planned for 29-30 June 1994
at St. John's College, University of Cambridge, UK in association with
BCS FACS. A Call for Papers (now closed) has been issued and is
available in the Z archive (see above) in the file "cfp94-2". For             |
general enquiries, contact the Conference Chair, Jonathan Bowen, on           |
<[e-mail]> (tel [phone], fax [phone]).    |
  The 6th International Conference on Formal Description Techniques
was held at Boston, Massachusetts, USA on 26-29 October 1993.                 |
FORTE'93 addressed formal techniques and testing methodologies                |
applicable to Distributed Systems such as Estelle, Lotos, SDL, ASN.1,
Z, etc. For further information, contact Richard L. Tenney (Chair),
Math & Computer Science, University of Massachusetts, Boston, MA
02125-3393, USA (email <[e-mail]>).
  The BCS FACS 5th Refinement Workshop was held on 8-10 January 1992,         |
at Lloyd's Register of Shipping, Fenchurch Street, London, England.
The proceedings are published in the Springer-Verlag Workshops in             |
Computing series. The 6th Refinement Workshop will be held at City
University, London, UK, 5-7 January 1994. Contact the Programme Chair,
David Till, Dept of Computer Science, City University, Northampton
Square, London, EC1V 0HB, UK (tel [phone] email
<[e-mail]>) for further information. For general information        |
information on the BCS FACS (British Computer Society Formal Aspects of       |
Computer Science) special interest group, email <[e-mail]>              |
(tel [phone], fax [phone]).                                     |
  The first FME (Formal Methods Europe) Symposium was be held at
Odense, Denmark, 19-23 April 1993.  The proceedings are available as
Springer LNCS 670. The next FME Symposium will be held 24-28 October          |
1994 in Barcelona, Spain.  The Programme Chair is Tim Denvir (tel             |
[phone], fax [phone], email <[e-mail]>)   |
and the Organizing Chair is Daniel Cabedo (tel [phone], fax            |
[phone], email <[e-mail]>). The chairman of          |
FME is Martyn Thomas, Praxis plc, 20 Manvers Street, Bath BA1 1PX, UK
(tel [phone], email <[e-mail]>).
  Details of Z-related meetings may be advertised on comp.specification.z
if desired. All the above meetings are likely to be repeated in some form.

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 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.

Subject: How can I obtain the 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 PostScript format.
Version 1.0 of the draft standard is accessible as "zstandard1.0.ps"
together with the appendices in "zstandard-annex1.0.ps".  It is also
available in printed form from the Oxford University Computing
Laboratory librarian on <[e-mail]> as 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) FACTS newsletter includes information
on Z. This is planned to be combined with an FME (Formal Methods
Europe) newsletter in the future.  Please send suitable material to the
Z column editor, David Till, Dept of Computer Science, City University,
Northampton Square, London, EC1V 0HB, UK (tel [phone] email
<[e-mail]>) 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: What if I've spotted a mistake or omission?

Updates: Please send corrections or new relevant information about
meetings, books, tools, etc., to <[e-mail]>.
New questions and model answers are also gratefully received!

--
Jonathan Bowen, <[e-mail]>
Programming Research Group, Oxford University Computing Laboratory, UK.