Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!zaphod.mps.ohio-state.edu!swrinde!elroy.jpl.nasa.gov!decwrl!ads.com!saturn!rar
From: rar@saturn.ads.com (Bob Riemenschneider)
Newsgroups: comp.specification.z
Subject: Re: What is this group (was Test)
Message-ID: <RAR.91Jun27122345@saturn.ads.com>
Date: 27 Jun 91 17:23:45 GMT
References: <2161@uqcspe.cs.uq.oz.au> <richard.677975691@mungarra>
	<1991Jun27.042414.7381@mlb.semi.harris.com>
	<CNH5730.91Jun27093615@calvin.tamu.edu>
Sender: usenet@ads.com (USENET News)
Organization: Advanced Decision Systems, Mountain View, CA 94043, +1 (415)
	960-7300
Lines: 51
In-Reply-To: cnh5730@calvin.tamu.edu's message of 27 Jun 91 14:36:15 GMT

In article <CNH5730.91Jun27093615@calvin.tamu.edu> cnh5730@calvin.tamu.edu (Charles Herrick) writes:

   In article <1991Jun27.042414.7381@mlb.semi.harris.com> john@mintaka.mlb.semi.harris.com (John M. Blasik) writes:
      Z, based on set theory and first
      order predicate logic, has been developed [... non-descriptive
      historical treatise deleted ...]

   Please elaborate, I don't understand the synopsis! (Of course, in that
   case, perhaps it's none of my business...) [;-}

Z is used to define set-theoretic models of a system that serve as
a formal specification.  An example might make things clearer

Here's an ACSII approximation of a piece of a Z specification of a
symbol table, the specification of the LookUp procedure:


    LookUp -----------------------------------------------
    |                                                    | 
    | st, st': SYM o-> VAL
    | s?: SYM
    | v!: VAL
    |
    |--------------------------------
    |
    | s? in dom(st) &
    | v! = st(s?) &
    | st' = st
    |                                                    |
    ------------------------------------------------------

The symbol table is modeled as a partial function from symbols to 
values.  st is the map representing the symbol table before the
operation is performed, st' represents the symbol table after.
(This use of the prime is a standard convention.)  s? represents 
the symbol whose value is sought.  (The use of a question mark in
the name of an input variable is another standard convention.)
v! represents that value.  (Exclamation mark for output.)  The
formula below the line just says what lookup must do -- return the
right value and not affect the contents of the table.  This particular
formula is very simple, but Z allows all the constructs of first-order
set theory to appear here (including unbounded quantification.)

This is particular example is trivial, of course, but real systems can
be and have been specified using this notation.  See Ian Hayes (ed.),
_Specification Case Studies_, Prentice-Hall, 1987, for a collection of
specifications, and J. M. Spivey, _The Z Notation: A Reference
Manual_, Prentice-Hall, 1989, for a complete description of the
notation.

							-- rar