🚀 go-pugleaf

anthony@cs.uq.oz.au (Anthony Lee) writes:

>This is a test to see if this is a real group.
>Noted the distribution.

Well it didn't work... I got it in Melbourne, I wonder if 'uq' distribution
is actually recognised by anyone.  


Anyone know what this group is about? (I've always wanted to ask this!)

--

Richard Begg (richard@asis.unimelb.edu.au)
Programmer ASIS/ITS - University of Melbourne

richard@mungarra.asis.unimelb.edu.au (Richard Begg) writes:
>anthony@cs.uq.oz.au (Anthony Lee) writes:
>
>>This is a test to see if this is a real group.
>>Noted the distribution.
>
>Well it didn't work... I got it in Melbourne, I wonder if 'uq' distribution
>is actually recognised by anyone.  

I think uq must be the Melbourne distrubution or something.

>Anyone know what this group is about? (I've always wanted to ask this!)

From the control message:

comp.specification.z is an unmoderated newsgroup which passed its vote for
creation by 194:40 as reported in news.announce.newgroups on 19 Jun 1991.

For your newsgroups file:
comp.specification.z	Discussion about the formal specification notation Z.

The charter, culled from the call for votes:

Comp.specification.z is intended to handle messages concerned with the
formal specification notation Z. Z, based on set theory and first
order predicate logic, has been developed at the Programming Research
Group (PRG) at Oxford University 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
standardization. Comp.specification.z would provide a convenient forum
for messages concerned with recent developments and the use of Z.


>
>--
>
>Richard Begg (richard@asis.unimelb.edu.au)
>Programmer ASIS/ITS - University of Melbourne

-- john@mlb.semi.harris.com

>>>>> On 27 Jun 91 04:24:14 GMT, john@mintaka.mlb.semi.harris.com (John M. Blasik) said:

John> The charter, culled from the call for votes:

John> Comp.specification.z is intended to handle messages concerned with the
John> formal specification notation Z. Z, based on set theory and first
John> order predicate logic, has been developed at the Programming Research
John> Group (PRG) at Oxford University for well over a decade. It is now
John> used by industry as part of the software (and hardware) development
John> process in both the UK and the US. It is currently undergoing
John> standardization. Comp.specification.z would provide a convenient forum
John> for messages concerned with recent developments and the use of Z.

Could someone post a list of references to Z for those of us that want
to bone up on this?  Thanks
--

    -- Andy Crump

    ...!tektronix!reed!littlei!andyc | andyc@littlei.intel.com
    ...!uunet!littlei!andyc          | andyc@littlei.uu.net

Disclaimer: Any opinions expressed here are my own and 
            not representive of Intel Corportation.

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...) [;-}

--
"I am walking on the wire
 and the wire is what the whole thing is about."
 -- John Stewart

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

People,

	I was interested in Z a while back when I was writing a paper
	on Object Oriented Analysis and Design.

	This group is sure to re-spark my interest.

	Here is a good introductory text that provides several chapters
	on the Z specification language.

	"An Introduction to Discrete Mathematics and Formal System
	Specification", D.C. INCE, Open University.  Claredon Press,
	Oxford, 1988.

	There are three parts to the book.  Part I deals with software
	development.  Part II deals with Prop. and Pred. Calculus, and
	Set Theory. Part III deals with Z and contains the
	following chapters,

		9  The Specification Lanuguage Z
		10 Operators and Objects in Z
		11 The Z Schema Calculus
		12 Z Specifications in Action - The University of
		   Lincoln Library System

		APPENDIX: Definition of Z Operators

	Regards |(8>
---
Robert
rdthomps@vela.acs.oakland.edu

In <7559@vela.acs.oakland.edu> rdthomps@vela.acs.oakland.edu (Robert D. Thompson) writes:

>People,

>	I was interested in Z a while back when I was writing a paper
>	on Object Oriented Analysis and Design.
[refs deleted]

	Perhaps you might be interested in Object-Z. The object-oriented
	version of Z developed here at the University of Queensland. 

	Sure beats plain old Z.

*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*

EMAIL: thomo@cs.uq.oz.au 			Ph: (07) 365 2726

SNAIL: John Thomas,         	               +------------------+
       c/o Computer Science Department,        |   And remember,  |
       University of Queensland,               | A HONKED nose is |
       Queensland, 4072 Australia. 	       |  a HAPPY nose !  |
                            	               +------------------+
*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*

In article <2193@uqcspe.cs.uq.oz.au> thomo@cs.uq.oz.au (John Thomas) writes:
	   Perhaps you might be interested in Object-Z. The object-oriented
	   version of Z developed here at the University of Queensland. 

Oh, please, tell us more, tell us more!!! 
(;-]
	seriously...
--
"I am walking on the wire
 and the wire is what the whole thing is about."
 -- John Stewart

cnh5730@calvin.tamu.edu (Charles Herrick) writes:

>In article <2193@uqcspe.cs.uq.oz.au> thomo@cs.uq.oz.au (John Thomas) writes:
>	   Perhaps you might be interested in Object-Z. The object-oriented
>	   version of Z developed here at the University of Queensland. 

>Oh, please, tell us more, tell us more!!! 
>	seriously...

Object-Z is a model-oriented specification language (like Z, VDM and the
Relational Notation of S. Lam and A.U. Shankar).  Object-Z is an extension
to Z which supports an object-oriented style of specification.

The Version 1 reference manual for Object-Z can be obtained by emailing your
normal (i.e. non-electronic) mail address to the Formal Methods Group librarian
at the Department of Computer Science, University of Queensland:

fmg@cs.uq.oz.au

-----------------
Formal Methods Group librarian
Department of Computer Science
University of Queensland
AUSTRALIA 4072