richard@mungarra.asis.unimelb.edu.au (Richard Begg) (06/27/91)
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
john@mintaka.mlb.semi.harris.com (John M. Blasik) (06/27/91)
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
andyc@bucky.intel.com (Andy Crump) (06/27/91)
>>>>> 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.cnh5730@calvin.tamu.edu (Charles Herrick) (06/27/91)
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 Stewartianf@chook.ua.oz (Ian Florance) (06/27/91)
> 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 Hmmmm, you may have to be more more specific in your question. eg What is the intended aims of this group? What is the definition of the 'comp.specification.z'? What are the criteria for articles to be accepted in this news group? ___________________________________________ _--_|\ Ian Florance Phone : +6 18 228 5502 / \ The Univeristy of Adelaide Apple Consortium \_.--*_/ University of Adelaide, South Australia v
rar@saturn.ads.com (Bob Riemenschneider) (06/28/91)
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
cnh5730@calvin.tamu.edu (Charles Herrick) (06/28/91)
-- "I am walking on the wire and the wire is what the whole thing is about." -- John Stewart