From ox-prg!prg.ox.ac.uk!bowen Thu Jun 27 15:52:17 BST 1991 Status: RO Article 1 of comp.specification.z: Path: ox-prg!prg.ox.ac.uk!bowen >From: bowen@prg.ox.ac.uk (Jonathan Bowen) Newsgroups: comp.specification.z Subject: Welcome to comp.specification.z Message-ID: <1927@culhua.prg.ox.ac.uk> Date: 27 Jun 91 14:45:24 GMT Sender: news@prg.ox.ac.uk Reply-To: zforum-request@prg.ox.ac.uk Organization: Programming Research Group, Oxford University, UK Lines: 85 The comp.specification.z newsgroup has now been created. It is unmoderated and messages posted on the newsgroup will be automatically posted to the Z FORUM mailing list as well. Mailing list subscribers can still post to the list by sending an e-mail message to . Messages will now be forwarded immediately to the mailing list and as well the comp.specification.z newsgroup. Mailing list subscribers who can access comp.specification.z may unsubscribe from ZFORUM by sending a short message to that effect to . Below is the charter for the newsgroup and an extract of the message which is sent out to Z FORUM subscribers. Thank you to all those who took part in the vote. -- Jonathan Bowen, PRG, Oxford. NAME: comp.specification.z STATUS: unmoderated PURPOSE: Discussion concerning with the formal specification notation Z. For the complete charter, motivation, etc., please see below. Charter: 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 provides a convenient forum for messages concerned with recent developments and the use of Z. Mailing list: There is a Z FORUM mailing list. Articles are automatically cross-posted between comp.specification.z and the mailing list for those whose do not have access to USENET news. This applied particularly to our industrial subscribers who we wish to encourage. Contact with your name, address and e-mail address to join the mailing list. Archive: There is a mail-based electronic archive server at the PRG which contains all the back-issues and messages on Z FORUM, as well as a selection of other Z-related files. I would plan to continue to archive messages on "comp.specification.z" on this server. (Send a message containing the command "help" to for further information.) For information on back issues and other Z-related files, send a message containing the command "help" to in the first instance. (The PRG archive server is a simple program capable of sending a number of archived files via e-mail.) Send submissions for ZFORUM to the moderator on . If you change your e-mail address or wish to be removed from the list, please e-mail . VDM'91 will be held on 21-25 October, 1991 in the Netherlands. The meeting will include papers on Z. For further information, please e-mail the command "send z vdm91" to the PRG archive server. This year's Z User Meeting will be held in December at York University. Details will be distributed via Z FORUM. Information on Programming Research Group (PRG) Technical Monographs and Reports, including many on Z, is available from our librarian on . If you are currently using Z, you are welcome to introduce yourself 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 annual Z User Meetings held each December in the UK. If you wish to join the postal Z mailing list, please send your address to the industrial liaison secretary at the PRG in Oxford on . -- Jonathan Bowen, Programming Research Group, Oxford University Computing Laboratory, UK. -- Jonathan Bowen, Oxford University Computing Laboratory. From ox-prg!prg.ox.ac.uk!bowen Thu Jun 27 18:54:20 BST 1991 Article: 2 of comp.specification.z Path: ox-prg!prg.ox.ac.uk!bowen From: bowen@prg.ox.ac.uk (Jonathan Bowen) Newsgroups: comp.specification.z Subject: Test message local to Oxford only Message-ID: <1928@culhua.prg.ox.ac.uk> Date: 27 Jun 91 17:52:07 GMT Sender: news@prg.ox.ac.uk Distribution: local Organization: Programming Research Group, Oxford University, UK Lines: 6 Status: O Testing the comp.specification.z and ZFORUM mailing list configuration. Please ignore. -- Jonathan Bowen, Oxford University Computing Laboratory. From ox-prg!prg.ox.ac.uk!bowen Thu Jun 27 18:57:12 BST 1991 Article: 3 of comp.specification.z Path: ox-prg!prg.ox.ac.uk!bowen From: bowen@prg.ox.ac.uk (Jonathan Bowen) Newsgroups: comp.specification.z Subject: 2nd local test Message-ID: <1929@culhua.prg.ox.ac.uk> Date: 27 Jun 91 17:57:04 GMT Sender: news@prg.ox.ac.uk Distribution: local Organization: Programming Research Group, Oxford University, UK Lines: 5 Status: O Please ignore. -- Jonathan Bowen, Oxford University Computing Laboratory. From ox-prg!ukc!mcsun!uunet!cs.utexas.edu!helios!cnh5730 Sun Jun 30 17:56:34 BST 1991 Article: 7 of comp.specification.z Path: ox-prg!ukc!mcsun!uunet!cs.utexas.edu!helios!cnh5730 From: cnh5730@calvin.tamu.edu (Charles Herrick) Newsgroups: comp.specification.z Subject: Re: What is this group (was Test) Message-ID: Date: 28 Jun 91 14:50:05 GMT References: <3865@sirius.ucs.adelaide.edu.au> Sender: usenet@helios.TAMU.EDU Organization: Texas A&M University Lines: 4 In-reply-to: ianf@chook.ua.oz's message of 27 Jun 91 15:54:40 GMT Status: O -- "I am walking on the wire and the wire is what the whole thing is about." -- John Stewart From ox-prg!ukc!mcsun!uunet!cs.utexas.edu!helios!cnh5730 Sun Jun 30 17:56:59 BST 1991 Article: 8 of comp.specification.z Path: ox-prg!ukc!mcsun!uunet!cs.utexas.edu!helios!cnh5730 From: cnh5730@calvin.tamu.edu (Charles Herrick) Newsgroups: comp.specification.z Subject: Re: Obj-Orien. Z, was: HERE'S A GOOD INTRO. TEXT Message-ID: Date: 28 Jun 91 14:53:16 GMT References: <2161@uqcspe.cs.uq.oz.au> <1991Jun27.042414.7381@mlb.semi.harris.com> <7559@vela.acs.oakland.edu> <2193@uqcspe.cs.uq.oz.au> Sender: usenet@helios.TAMU.EDU Organization: Texas A&M University Lines: 11 In-reply-to: thomo@cs.uq.oz.au's message of 28 Jun 91 00:25:43 GMT Status: O 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 From ox-prg!ukc!mcsun!uunet!munnari.oz.au!bunyip.cc.uq.oz.au!uqcspe!cs.uq.oz.au!fmg Sun Jun 30 17:57:26 BST 1991 Article: 9 of comp.specification.z Path: ox-prg!ukc!mcsun!uunet!munnari.oz.au!bunyip.cc.uq.oz.au!uqcspe!cs.uq.oz.au!fmg From: fmg@cs.uq.oz.au ( Fuzzy Memory Group) Newsgroups: comp.specification.z Subject: Re: Obj-Orien. Z, was: HERE'S A GOOD INTRO. TEXT Message-ID: <2221@uqcspe.cs.uq.oz.au> Date: 28 Jun 91 16:31:42 GMT References: <2161@uqcspe.cs.uq.oz.au> <1991Jun27.042414.7381@mlb.semi.harris.com> <7559@vela.acs.oakland.edu> <2193@uqcspe.cs.uq.oz.au> Sender: news@cs.uq.oz.au Reply-To: fmg@cs.uq.oz.au Lines: 24 Status: O 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 From ox-prg!ukc!mcsun!uunet!munnari.oz.au!bunyip.cc.uq.oz.au!uqcspe!cs.uq.oz.au!fmg Sun Jun 30 17:57:53 BST 1991 Article: 10 of comp.specification.z Path: ox-prg!ukc!mcsun!uunet!munnari.oz.au!bunyip.cc.uq.oz.au!uqcspe!cs.uq.oz.au!fmg From: fmg@cs.uq.oz.au ( Fuzzy Memory Group) Newsgroups: comp.specification.z Subject: Re: Obj-Orien. Z, was: HERE'S A GOOD INTRO. TEXT Message-ID: <15323.9106300647@prg.ox.ac.uk> Date: 30 Jun 91 06:47:26 GMT References: <2161@uqcspe.cs.uq.oz.au> <1991Jun27.042414.7381@mlb.semi.harris.com> <7559@vela.acs.oakland.edu> <2193@uqcspe.cs.uq.oz.au> Original-Date: 28 Jun 91 16:31:42 GMT X-Mailer: mail-news 2.0.3 X-Mailer: mail-news 2.0.3 Status: O @calvin.tamu.edu> Original-Sender: news@cs.uq.oz.au Reply-To: fmg@cs.uq.oz.au Approved: zforum@prg.oxford.ac.uk Lines: 24 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 From ox-prg!ukc!mcsun!uunet!europa.asd.contel.com!noc.sura.net!haven.umd.edu!uvaarpa!software.org!blakemor Sun Jun 30 17:59:23 BST 1991 Article: 11 of comp.specification.z Path: ox-prg!ukc!mcsun!uunet!europa.asd.contel.com!noc.sura.net!haven.umd.edu!uvaarpa!software.org!blakemor From: blakemor@software.org (Alex Blakemore) Newsgroups: comp.specification.z Subject: Re: What is this group - HERE'S A GOOD INTRO. TEXT ON 'Z'... Message-ID: <1991Jun28.160145.8626@software.org> Date: 28 Jun 91 16:01:45 GMT References: <1991Jun27.042414.7381@mlb.semi.harris.com> <7559@vela.acs.oakland.edu> <2193@uqcspe.cs.uq.oz.au> Organization: Software Productivity Consortium, Herndon, Virginia Lines: 10 Status: O In article <2193@uqcspe.cs.uq.oz.au> thomo@cs.uq.oz.au writes: > Perhaps you might be interested in Object-Z. The object-oriented > version of Z developed here at the University of Queensland. how about some references or an anonymous ftp site for papers describing object-z. sounds interesting. -- --------------------------------------------------------------------- Alex Blakemore blakemore@software.org (703) 742-7125 Software Productivity Consortium 2214 Rock Hill Rd, Herndon VA 22070 From ox-prg!ukc!mcsun!uunet!stanford.edu!agate!lima.berkeley.edu!bks Sun Jun 30 18:00:00 BST 1991 Article: 12 of comp.specification.z Path: ox-prg!ukc!mcsun!uunet!stanford.edu!agate!lima.berkeley.edu!bks From: bks@lima.berkeley.edu (Bradley K. Sherman) Newsgroups: comp.specification.z Subject: Prove me wrong Message-ID: <1991Jun28.175058.4987@agate.berkeley.edu> Date: 28 Jun 91 17:50:58 GMT Sender: usenet@agate.berkeley.edu (USENET Administrator) Organization: University of California at Berkeley Lines: 17 Originator: bks@lima.berkeley.edu Status: O Z will never emerge as a useful tool for real-world programmers and analysts because it cannot be expressed on glass tty's. Back to the drawing board and come up with an unambiguous syntax expressible in the intersection of the ASCII and EBCDIC codes and we can make some progress. We just don't have the time to muck with Troff or Latex just to write down our specs for the systems. Also we'd like to see the specs online. Is this too much to ask? ---------------------- Brad Sherman (bks@alfa.berkeley.edu) Just trying to get your juices flowing. Good luck with your new group. From ox-prg!ukc!mcsun!uunet!munnari.oz.au!bunyip.cc.uq.oz.au!uqcspe!cs.uq.oz.au!thomo Sun Jun 30 18:01:27 BST 1991 Article: 13 of comp.specification.z Path: ox-prg!ukc!mcsun!uunet!munnari.oz.au!bunyip.cc.uq.oz.au!uqcspe!cs.uq.oz.au!thomo From: thomo@cs.uq.oz.au (John Thomas) Newsgroups: comp.specification.z Subject: Re: Prove me wrong Message-ID: <2222@uqcspe.cs.uq.oz.au> Date: 29 Jun 91 00:52:28 GMT References: <1991Jun28.175058.4987@agate.berkeley.edu> Sender: news@cs.uq.oz.au Reply-To: thomo@cs.uq.oz.au Lines: 57 Status: O In <1991Jun28.175058.4987@agate.berkeley.edu> bks@lima.berkeley.edu (Bradley K. Sherman) writes: >Z will never emerge as a useful tool for real-world programmers and >analysts because it cannot be expressed on glass tty's. >Back to the drawing board and come up with an unambiguous syntax >expressible in the intersection of the ASCII and EBCDIC codes >and we can make some progress. >We just don't have the time to muck with Troff or Latex just to write >down our specs for the systems. Also we'd like to see the specs online. >Is this too much to ask? No, it's not too much to ask ! After all, how long does it take to do something in latex ? Ans: Close to forever. The real world just won't stand still while you go and 'latex' the specs. But then again, how often do you end up with software that doesn't meet its specification. Or worse yet, according to the USERS it isn't what they wanted. Specification languages like Z may result (altough ALL software should have some form of specification, even if it's in ENGLISH) in a project taking longer to complete overall BUT at the end of the day you will HAVE software which meets its spec. since Z (or whatever you choose to use) states PRECISELY what is required, no IFS or BUTS about it. So the extra (?) time spent writing the spec. in Z (or whatever) will probably pay dividends during the lifetime of the software since you not only have software which does what it's meant to but in case of future modifications to it, the Z specs also serve as documentation. I also believe there is some kind of Z editor somewhere here at the University of Qld Anyone from University of QLD care to comment ? Yep, I think thats just about my $0.02 worth for today. Writing for TRUTH, JUSTICE and CRUELTY (but mainly cruelty), *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-* 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 ! | +------------------+ *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-* From ox-prg!ukc!mcsun!uunet!munnari.oz.au!bunyip.cc.uq.oz.au!uqcspe!cs.uq.oz.au!rhys Sun Jun 30 18:02:58 BST 1991 Article: 14 of comp.specification.z Path: ox-prg!ukc!mcsun!uunet!munnari.oz.au!bunyip.cc.uq.oz.au!uqcspe!cs.uq.oz.au!rhys From: rhys@cs.uq.oz.au (Rhys Weatherley) Newsgroups: comp.specification.z Subject: Re: Prove me wrong Message-ID: <2223@uqcspe.cs.uq.oz.au> Date: 29 Jun 91 01:47:00 GMT References: <1991Jun28.175058.4987@agate.berkeley.edu> Sender: news@cs.uq.oz.au Reply-To: rhys@cs.uq.oz.au Lines: 36 Status: O In <1991Jun28.175058.4987@agate.berkeley.edu> bks@lima.berkeley.edu (Bradley K. Sherman) writes: >Back to the drawing board and come up with an unambiguous syntax >expressible in the intersection of the ASCII and EBCDIC codes >and we can make some progress. >We just don't have the time to muck with Troff or Latex just to write >down our specs for the systems. Also we'd like to see the specs online. How about a graphics-based Z editor under SunView or X/Windows? There are people here at UQ working on such a beast and it's quite trendy. You can mix explanatory text, Z specs and even code if you like. But it's still coming along at the moment. ASCII and EBCDIC terminals are quickly going the way of the dinosaur with graphics terminals, high-resolution PC's, etc, becoming more common-place. As for sending such specs through the mail, etc, the new mail format Internet Draft specifies how you can send images, TeX documents, etc through the mail and have them intelligently processed and displayed at the other end, so that's not a problem either anymore. (Given a year or two for the mail and news readers to be updated :-). As this progresses you won't need to think in ASCII or EBCDIC anymore, but documents, so Z will fit in no worries with the emerging editors and mail processing standards. Think of writing a Z spec (or any spec for that matter) as being an exercise in desktop publishing. Cheers, Rhys. +=====================+==================================+ || Rhys Weatherley | The University of Queensland, || || rhys@cs.uq.oz.au | Australia. G'day!! || || "I'm a FAQ nut - what's your problem?" || +=====================+==================================+ From ox-prg!ukc!mcsun!uunet!spool.mu.edu!munnari.oz.au!bunyip.cc.uq.oz.au!uqcspe!cs.uq.oz.au!david Wed Jul 3 13:40:25 BST 1991 Status: O Article 15 of comp.specification.z: Path: ox-prg!ukc!mcsun!uunet!spool.mu.edu!munnari.oz.au!bunyip.cc.uq.oz.au!uqcspe!cs.uq.oz.au!david >From: david@cs.uq.oz.au (David Duke) Newsgroups: comp.specification.z Subject: Re: Prove me wrong Message-ID: <2232@uqcspe.cs.uq.oz.au> Date: 30 Jun 91 23:43:36 GMT References: <1991Jun28.175058.4987@agate.berkeley.edu> Sender: news@cs.uq.oz.au Reply-To: david@cs.uq.oz.au Lines: 64 In <1991Jun28.175058.4987@agate.berkeley.edu> bks@lima.berkeley.edu (Bradley K. Sherman) writes: >Z will never emerge as a useful tool for real-world programmers and >analysts because it cannot be expressed on glass tty's. Oh? \begin{schema}{table} data : Key \ffun Value \\ keys : \fset Key \\ \ST \dom data = keys \end{schema} :-) :-) Seriously though, using the fuzz or oz macros with LaTeX, Z is not all that unreadable. It is also not to difficult to come up with ascii `lookalikes' for many of the symbols in the standard library; I often use such approximations when sending questions involving Z text by mail. e.g. \dom ==> dom \tfun ==> -> \pfun ==> +> \ffun ==> ++> \dres ==> <| \limg ==> (| etc Perhaps someone has proposed a a standard set of these? The variety of box notations is more of a problem, but perhaps you could use just the latex \begin{...} and \end{...} delimiters? >Back to the drawing board and come up with an unambiguous syntax >expressible in the intersection of the ASCII and EBCDIC codes >and we can make some progress. Whats ambiguous about the syntax? There are several type checkers available for Z (for example, `Fuzz' by Mike Spivey at the PRG, Oxford Uni); there is also a syntax-based editor at UQ -- all of which need a precise syntax on which to work! >We just don't have the time to muck with Troff or Latex just to write >down our specs for the systems. Also we'd like to see the specs online. Do you mean you don't have time to install/learn LaTeX, or you find it too difficult to write Z specs *in* LaTeX; is the latter, have you looked at the macro packages zed.sty and oz.sty? >Is this too much to ask? IMHO, the concise notation is one of the attractions of Z, and part of the attraction is the use of standard mathematical symbols -- yes, there are some peculiar to Z, but I did not find them hard to learn once you note their regularity. Replacing these with ascii equivalents may help those with acess only to ascii terminals, but I don't think that this would suddenly make it more popular or accessible. >---------------------- > Brad Sherman (bks@alfa.berkeley.edu) David Duke. david@cs.uq.oz.au From ox-prg!ukc!mcsun!uunet!munnari.oz.au!bunyip.cc.uq.oz.au!uqcspe!cs.uq.oz.au!brendan Wed Jul 3 13:41:33 BST 1991 Status: O Article 16 of comp.specification.z: Path: ox-prg!ukc!mcsun!uunet!munnari.oz.au!bunyip.cc.uq.oz.au!uqcspe!cs.uq.oz.au!brendan >From: brendan@cs.uq.oz.au (Brendan Mahony) Newsgroups: comp.specification.z Subject: Re: Prove me wrong Message-ID: <2235@uqcspe.cs.uq.oz.au> Date: 1 Jul 91 00:24:13 GMT References: <1991Jun28.175058.4987@agate.berkeley.edu> <2232@uqcspe.cs.uq.oz.au> Sender: news@cs.uq.oz.au Reply-To: brendan@cs.uq.oz.au Lines: 59 In <1991Jun28.175058.4987@agate.berkeley.edu> bks@lima.berkeley.edu (Bradley K. Sherman) writes: >>Back to the drawing board and come up with an unambiguous syntax >>expressible in the intersection of the ASCII and EBCDIC codes >>and we can make some progress. In <2232@uqcspe.cs.uq.oz.au> david@cs.uq.oz.au (David Duke) writes: >Whats ambiguous about the syntax? There are several type checkers available >for Z (for example, `Fuzz' by Mike Spivey at the PRG, Oxford Uni); there is >also a syntax-based editor at UQ -- all of which need a precise syntax on >which to work! I am afraid this is not much of an argument. Both these parsers use a restricted Z grammar. Yes I know Spivey's is "definitive", but it is still a re-engineering of the language and is much more restrictive than what people used to write down before there was an official syntax. The UQ grammar (and it seems the Spivey one) is a linearised version of Z. This means that you either have to put in more brackets than you would like, or you must define precedents between operators that cannot interfer semantically, such as + and union or more importantly function application and function application. An expression like f g a can generally only mean one thing, either f : (X -> Y) -> (A -> B) g : X -> Y a : A f g a = (f(g))(a) : B example: f^3 x or f : Y -> Z g : X -> Y a : X f g a = f(g(a)) : Z example: sin cos x If either meaning is clear from the context, then the parser should chose the right one regardless of precedent information. You should not have to put brackets in to "force" the parser to read it the right way. If neither meaning is clear from the context, for example an expression involving type conformant expressions such as {} {} {} then your really do have an ambiguity and it should be flagged as such and not hidden by magical precedent applications. -- Brendan Mahony | brendan@batserver.cs.uq.oz Department of Computer Science | heretic: someone who disgrees with you University of Queensland | about something neither of you knows Australia | anything about. From ox-prg!brianm Wed Jul 3 13:43:39 BST 1991 Status: O Article 17 of comp.specification.z: Path: ox-prg!brianm >From: brianm@cs.man.ac.uk (Brian Monahan) Newsgroups: comp.specification.z Subject: BSI/VDM vs Z notation ... again! Message-ID: <9107011158.AA02241@r8h.cs.man.ac.uk> Date: 1 Jul 91 11:58:43 GMT Sender: daemon@prg.ox.ac.uk Lines: 52 X-Mailer: mail-news 2.0.3 I would like to try and help clear up one or two small misconceptions about VDM that surfaced recently in the "VDM vs Z notation" debate. A standard for VDM is being put together under the auspices of the BSI and will go forward, in due course, for consideration as an international standard by ISO. At present, the notation being standardised is known as BSI/VDM. It is true that the standard has been expected for some time - but as work must proceed towards ISO standardisation, it is now under some pressure to converge. Although I should emphasise that I am no longer directly involved in the development of this work, I understand that the main effort has been on *formal semantics* and in converging the syntax of the 2 main dialects of VDM. The main issue lies in trying to converge the 2 distinct styles of specification and description that VDM has contained in the past. The implicit, relational style (Jones's pre/post conditions over state pairs) and the explicit, imperative techniques used for compiler design and algorithm description. As a result, BSI/VDM is therefore a wide-spectrum *notation*, from predicate logic based specification on the one hand, to functional and imperative programming on the other. It is important *not* to confuse the notation itself with development techniques, concepts of data reification and operation decomposition, each of which were pioneered (for model based specification) within the VDM framework by Jones (1980 and 1986 books). This topic is also being actively pursued in Z (c.f. Morgan's work on refinement in Z and also Nipkow's theoretical work for VDM). As far as I am aware, BSI/VDM has no (direct) connection with the SADT notation, a diagram-based requirements capture technique. Finally, there is an chapter called "Model Based Specifications" (by myself and Roger Shaw) in the "Software Engineers Reference Book" (edited by John McDermid), published by Butterworth-Heinemann, May 1991, which contains a substantial case study in Z, followed by a discussion of the respective trade-offs in specification between Z and VDM. /////////////////////////////////////////////////////////////////////// / Dr. Brian Monahan / / Department of Computer Science / E-mail : brianm@cs.man.ac.uk The University of Manchester / bqm@cs.man.ac.uk Oxford Road / Phone : (+44)-61-275-6137 Manchester M13 9PL / (New) FAX : (+44)-61-275-6236 / /////////////////////////////////////////////////////////////////////// From ox-prg!bob Wed Jul 3 13:43:58 BST 1991 Status: O Article 18 of comp.specification.z: Path: ox-prg!bob >From: bob@cs.man.ac.uk (Bob Fields) Newsgroups: comp.specification.z Subject: Obj-Orien. Z, was: HERE'S A GOOD INTRO. TEXT Message-ID: <9107011250.AA01933@ipse4.cs.man.ac.uk> Date: 1 Jul 91 12:50:40 GMT Sender: daemon@prg.ox.ac.uk Lines: 18 In-Reply-To: Fuzzy Memory Group's message of Sun, 30 Jun 91 07:47:26 +0100 <15323.9106300647@prg.ox.ac.uk> X-Mailer: mail-news 2.0.3 | 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: I would be interested in a copy of the Object-z reference manual. Thanks. Bob fields. (bob@cs.man.ac.uk) ICL, Wenlock Way, West Gorton, Manchester, M12 5DR, U.K. From ox-prg!ananda Wed Jul 3 13:44:57 BST 1991 Status: O Article 19 of comp.specification.z: Path: ox-prg!ananda >From: ananda@csboojum.cov.ac.uk (Ananda Amatya (STAFF)) Newsgroups: comp.specification.z Subject: (none) Message-ID: <532.9107011642@csboojum.cov.ac.uk> Date: 1 Jul 91 16:42:25 GMT Sender: daemon@prg.ox.ac.uk Lines: 29 X-Mailer: mail-news 2.0.3 Subject: Obj-Orien. Z, was: HERE'S A GOOD INTRO.TXT Original-Message-Id: <9107011250.AA01933@ipse4.cs.man.ac.uk> Original-Date: 1 Jul 91 12:50:40 GMT Original-Sender: daemon@prg.ox.ac.uk In-Reply-To: Fuzzy Memory Group's message of Sun, 30 Jun 91 07:47:26 +0100 <15323.9106300647@prg.ox.ac.uk> Approved: zforum@prg.oxford.ac.uk Lines: 18 Status: R | 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: I would be interested in a copy of the Object-z reference manual. Thanks. Ananda Amatya. (ananda@csboojum.cov.ac.uk) Coventry Polytechnic Computer Science Dept. Priory Street Coventry CV1 5FB U.K. From ox-prg!Hongji.Yang Wed Jul 3 13:45:12 BST 1991 Status: O Article 20 of comp.specification.z: Path: ox-prg!Hongji.Yang >From: Hongji.Yang@durham.ac.uk (Yang Hongji) Newsgroups: comp.specification.z Subject: Re: (none) Message-ID: Date: 1 Jul 91 16:48:36 GMT Sender: daemon@prg.ox.ac.uk Lines: 15 X-Mailer: mail-news 2.0.3 I would be interested in a copy of the Object-z reference manual. Thanks. Hongji Yang, Computer Science, SEAS, University of Durham, South Road, Science Lab., Durham, DH1 3LE. England From ox-prg!ukc!mcsun!uunet!wang!harvee!esj Wed Jul 3 13:46:16 BST 1991 Status: O Article 21 of comp.specification.z: Path: ox-prg!ukc!mcsun!uunet!wang!harvee!esj >From: esj@harvee.UUCP (Eric S Johansson) Newsgroups: comp.specification.z Subject: Re: Prove me wrong Message-ID: <8763580@harvee.UUCP> Date: 30 Jun 91 22:30:54 GMT References: <1991Jun28.175058.4987@agate.berkeley.edu> Organization: gators 'r us Lines: 43 X-Version: Rodney's UUCP modules 02/11/90 V1.18 In article <1991Jun28.175058.4987@agate.berkeley.edu> bks@lima.berkeley.edu (Bradley K. Sherman) writes: > > Z will never emerge as a useful tool for real-world programmers and > analysts because it cannot be expressed on glass tty's. > > Back to the drawing board and come up with an unambiguous syntax > expressible in the intersection of the ASCII and EBCDIC codes > and we can make some progress. I trust Peter K. to correct me if I am wrong but I believe Bill Stoddart and Peter Knaggs have written a series of papers in which they do just what you want ( unambigous expression of Z in straight ascii) > > We just don't have the time to muck with Troff or Latex just to write > down our specs for the systems. Also we'd like to see the specs online. Call me twisted, but I find mucking in Latex less difficult that trying to coax MiserySoft Word (or any other WP for that matter) to speak Z. As for seeing specs on-line, I just fire up xdvi and there are my specs. No problem. > > ---------------------- > Brad Sherman (bks@alfa.berkeley.edu) > > Just trying to get your juices flowing. Good luck with your new group. Good idea, and when this topic runs dry, we can start talking about how to deal with fear and anger from those who are threatened by the thought of using any notation other than C for specifying programs. heheh. let's get this group off to a good usenet traditional start... --- eric -- ... ^^^ eric johansson UUCP ...!uunet!wang!harvee!esj esj@harvee.uucp * * a juggling fool AT&T (617) 577-4068 (w) o HAM ka1eec \_/ CSNET johansson%hydra@polaroid.com or hydra!johansson@polaroid.com source of the public's fear of the unknown since 1956 From ox-prg!NER034 Wed Jul 3 13:47:20 BST 1991 Status: O Article 22 of comp.specification.z: Path: ox-prg!NER034 >From: NER034@PRIME-A.TEES-POLY.AC.UK Newsgroups: comp.specification.z Subject: ASCII specifications Message-ID: <15637.9107021249@prg.oxford.ac.uk> Date: 2 Jul 91 10:47:49 GMT Sender: news@prg.ox.ac.uk Lines: 77 X-Mailer: mail-news 2.0.3 In article <12618.9107012115@prg.ox.ac.uk> eric johansson writes: | In article <1991Jun28.175058.4987@agate.berkeley.edu> bks@lima.berkeley.edu | (Bradley K. Sherman) writes: | > | > Z will never emerge as a useful tool for real-world programmers and | > analysts because it cannot be expressed on glass tty's. | > | > Back to the drawing board and come up with an unambiguous syntax | > expressible in the intersection of the ASCII and EBCDIC codes | > and we can make some progress. | | I trust Peter K. to correct me if I am wrong but I believe Bill Stoddart | and Peter Knaggs have written a series of papers in which they do just | what you want ( unambigous expression of Z in straight ascii) | Sorry, but you are wrong on this one Eric. I have just been updating Paul King's LaTeX style file for Object Z to make it compatible with Mike Spivey's new Zed style file. | > | > We just don't have the time to muck with Troff or Latex just to write | > down our specs for the systems. Also we'd like to see the specs online. | | Call me twisted, but I find mucking in Latex less difficult that trying | to coax MiserySoft Word (or any other WP for that matter) to speak Z. As | for seeing specs on-line, I just fire up xdvi and there are my specs. | No problem. | You don't have to know about LaTeX to produce Z specifications. There are now several people who have produced "Z Writers". Although these can produce LaTeX output on request. For an ASCII terminal you have little choice but to use something like LaTeX, however, if you have graphics capabilites then I am sure that Logica, IBM, Praxis, and others of that ilk will be happy to provide you with (sell you) a system for writing specifications in graphical form. Personally speaking I prefer to use this kind of graphical interface. It makes for a simple life (I am using Logica package). | > ---------------------- | > Brad Sherman (bks@alfa.berkeley.edu) | > | > Just trying to get your juices flowing. Good luck with your new group. | | Good idea, and when this topic runs dry, we can start talking about how | to deal with fear and anger from those who are threatened by the thought | of using any notation other than C for specifying programs. | Eric, with your involvement in Forth you should not be talking treason like this. Note, that the papers that you refereed to before, are for the formalisation of the Forth language. Rather like the recent ANS X3/X3J14 committee meeting I went to. | heheh. let's get this group off to a good usenet traditional start... | | --- eric | -- | ... | ^^^ eric johansson UUCP ...!uunet!wang!harvee!esj esj@harvee.uucp | * * a juggling fool AT&T (617) 577-4068 (w) | o HAM ka1eec | \_/ CSNET johansson%hydra@polaroid.com | or hydra!johansson@polaroid.com | source of the public's fear of the unknown since 1956 Peter Knaggs +-----------------------------+-----------------------------------------------+ ! School of Comp. & Maths., ! Janet: NER034 @ uk.ac.tees-poly ! ! Teesside Polytechnic, ! Bitnet: NER034 % tp.ac.uk @ UKACRL ! ! Middlesbrough, ! Internet: NER034 % tp.ac.uk @ cunyvm.cuny.edu ! ! Cleveland, England. TS1 3BA ! Uucp: NER034 % tpoly.ac.uk @ ukc.uucp ! !-----------------------------+-----------------------------------------------! ! It is not enough to do the right thing; one must also do it the right way. ! +-----------------------------------------------------------------------------+ From ox-prg!ukc!mcsun!uunet!munnari.oz.au!metro!socs.uts.edu.au!syzygy!xma Wed Jul 3 13:47:34 BST 1991 Status: O Article 23 of comp.specification.z: Path: ox-prg!ukc!mcsun!uunet!munnari.oz.au!metro!socs.uts.edu.au!syzygy!xma >From: xma@socs.uts.edu.au (X Ma) Newsgroups: comp.specification.z Subject: Re: Prove me wrong Message-ID: Date: 2 Jul 91 04:35:49 GMT References: <1991Jun28.175058.4987@agate.berkeley.edu> Lines: 17 bks@lima.berkeley.edu (Bradley K. Sherman) writes: >Z will never emerge as a useful tool for real-world programmers and >analysts because it cannot be expressed on glass tty's. I was told that more than 90% people in company (world or Australia?) use DFD (Data Flow Diagram) instead of Z or other formal techniques to develop their system. I am interested in hearing any opinions on it. Xianwu Ma ------------------------------------- School of Computing Sciences University of Technology, Sydney NSW 2007, Australia ------------------------------------- From ox-prg!ukc!axion!fmg!jcrw Wed Jul 3 14:06:53 BST 1991 Status: O Article 24 of comp.specification.z: Path: ox-prg!ukc!axion!fmg!jcrw >From: jcrw@fmg.bt.co.uk (Jeremy Wilson) Newsgroups: comp.specification.z Subject: Re: Prove me wrong Message-ID: <1991Jul2.105231.20473@fmg.bt.co.uk> Date: 2 Jul 91 10:52:31 GMT References: <1991Jun28.175058.4987@agate.berkeley.edu> Organization: British Telecom Lines: 46 In-Reply-To: xma@socs.uts.edu.au's message of 2 Jul 91 04:35:49 GMT xma@socs.uts.edu.au (Ma Xianwu) writes: > >I was told that more than 90% people in company (world or Australia?) use >DFD (Data Flow Diagram) instead of Z or other formal techniques to develop >their system. I am interested in hearing any opinions on it. > It is probably true that DFD's are very widely used and that at present there are few industrial or commercial mainstream development projects using Z or other formal techniques, although that is more supposition on my part than actual knowledge. ( I just have not heard of that many although the number is greater than zero.) What is perhaps more to the point is whether Z and DFD's do the same job. As far as I can understand DFD's are essentially an informal graphical descriptive technique. Their main beauty is that they are understandable (supposedly) to the customer. There are, however, many functional aspects of a system which are not described. In most so-called "methodologies" DFD's are supplemented by a plethora of other "notations", eg ERD's ELH's Nasi-Schnurliman (my apologies to the relevant inventors if I got their names wrong) diagrams , etc etc etc. Z or VDM on the other hand are languages with rigorously defined semantics and syntax. It is possible in such languages to build a mathematical model of the functional aspects of the system, which can then be analysed. Even if there is NO INTENTION AT ALL of deriving code rigorously from such a formal specification, benefit can be had from such an exercise. In fact descriptions using DFD's and ERD's can often be considerably clarified and errors detected by respecifying parts of them using Z. There may well a good argument for using DFD's and other graphical notations in conjunction with formal languages. Has anyone any thoughts about this? +---------------------------------+----------------------------------------+ ! Jeremy Wilson ! ! ! Room 303 ! email: jcrw@fmg.bt.co.uk ! ! BT Development and Procurement ! Telephone: 0473-224578 ! ! St Vincent House ! International: +44 473-224578 ! ! 1 Cutler Street ! Facsimile: 0473-210182 ! ! IPSWICH ! International: +44 473-224578 ! ! Suffolk IP1 1UX ! Telex: 987705 ! ! United Kingdom ! International: +51 987705 ! +---------------------------------+----------------------------------------+ From ox-prg!ukc!axion!fmg!jcrw Wed Jul 3 14:09:34 BST 1991 Status: O Article 24 of comp.specification.z: Path: ox-prg!ukc!axion!fmg!jcrw >From: jcrw@fmg.bt.co.uk (Jeremy Wilson) Newsgroups: comp.specification.z Subject: Re: Prove me wrong Message-ID: <1991Jul2.105231.20473@fmg.bt.co.uk> Date: 2 Jul 91 10:52:31 GMT References: <1991Jun28.175058.4987@agate.berkeley.edu> Organization: British Telecom Lines: 46 In-Reply-To: xma@socs.uts.edu.au's message of 2 Jul 91 04:35:49 GMT xma@socs.uts.edu.au (Ma Xianwu) writes: > >I was told that more than 90% people in company (world or Australia?) use >DFD (Data Flow Diagram) instead of Z or other formal techniques to develop >their system. I am interested in hearing any opinions on it. > It is probably true that DFD's are very widely used and that at present there are few industrial or commercial mainstream development projects using Z or other formal techniques, although that is more supposition on my part than actual knowledge. ( I just have not heard of that many although the number is greater than zero.) What is perhaps more to the point is whether Z and DFD's do the same job. As far as I can understand DFD's are essentially an informal graphical descriptive technique. Their main beauty is that they are understandable (supposedly) to the customer. There are, however, many functional aspects of a system which are not described. In most so-called "methodologies" DFD's are supplemented by a plethora of other "notations", eg ERD's ELH's Nasi-Schnurliman (my apologies to the relevant inventors if I got their names wrong) diagrams , etc etc etc. Z or VDM on the other hand are languages with rigorously defined semantics and syntax. It is possible in such languages to build a mathematical model of the functional aspects of the system, which can then be analysed. Even if there is NO INTENTION AT ALL of deriving code rigorously from such a formal specification, benefit can be had from such an exercise. In fact descriptions using DFD's and ERD's can often be considerably clarified and errors detected by respecifying parts of them using Z. There may well a good argument for using DFD's and other graphical notations in conjunction with formal languages. Has anyone any thoughts about this? +---------------------------------+----------------------------------------+ ! Jeremy Wilson ! ! ! Room 303 ! email: jcrw@fmg.bt.co.uk ! ! BT Development and Procurement ! Telephone: 0473-224578 ! ! St Vincent House ! International: +44 473-224578 ! ! 1 Cutler Street ! Facsimile: 0473-210182 ! ! IPSWICH ! International: +44 473-224578 ! ! Suffolk IP1 1UX ! Telex: 987705 ! ! United Kingdom ! International: +51 987705 ! +---------------------------------+----------------------------------------+ From ox-prg!ukc!mcsun!uunet!munnari.oz.au!yoyo.aarnet.edu.au!sirius.ucs.adelaide.edu.au!eeyore!tonyb Wed Jul 3 14:09:39 BST 1991 Status: O Article 25 of comp.specification.z: Path: ox-prg!ukc!mcsun!uunet!munnari.oz.au!yoyo.aarnet.edu.au!sirius.ucs.adelaide.edu.au!eeyore!tonyb >From: tonyb@eeyore.adelaide.edu.au (Tony Blakey) Newsgroups: comp.specification.z Subject: Re: Prove me wrong Message-ID: <3919@sirius.ucs.adelaide.edu.au> Date: 2 Jul 91 03:21:05 GMT References: <1991Jun28.175058.4987@agate.berkeley.edu> <2232@uqcspe.cs.uq.oz.au> Sender: news@ucs.adelaide.edu.au Reply-To: tonyb@cs.adelaide.edu.au Organization: Adelaide University, Computer Science Lines: 7 Nntp-Posting-Host: eeyore.cs.adelaide.edu.au Is any of this stuff (oz.sty fuzz.sty) etc available through ftp somewhere. Is any of the UQ stuff available electronically (as opposed to snail mail) ? I'd love to get hold of it. Antony Blakey Computer Science Adelaide University. From ox-prg!ukc!mcsun!uunet!zaphod.mps.ohio-state.edu!rphroy!caen!uakari.primate.wisc.edu!aplcen!boingo.med.jhu.edu!haven.umd.edu!uvaarpa!software.org!blakemor Wed Jul 3 15:37:49 BST 1991 Status: O Article 26 of comp.specification.z: Path: ox-prg!ukc!mcsun!uunet!zaphod.mps.ohio-state.edu!rphroy!caen!uakari.primate.wisc.edu!aplcen!boingo.med.jhu.edu!haven.umd.edu!uvaarpa!software.org!blakemor >From: blakemor@software.org (Alex Blakemore) Newsgroups: comp.specification.z Subject: Re: (none) Message-ID: <1991Jul2.160513.14254@software.org> Date: 2 Jul 91 16:05:13 GMT References: Organization: Software Productivity Consortium, Herndon, Virginia Lines: 17 I would be interested in a copy of the Object-z reference manual. P.S. what is the email address of the "librarian" so people can email rather than post requests ? Thanks. Alex Blakemore Software Productivity Consortium 2214 Rock Hill Rd Herndon VA 22070 (703) 742-7125 blakemore@software.org -- --------------------------------------------------------------------- Alex Blakemore blakemore@software.org (703) 742-7125 Software Productivity Consortium 2214 Rock Hill Rd, Herndon VA 22070 From ox-prg!bowen Wed Jul 3 15:39:59 BST 1991 Status: O Article 27 of comp.specification.z: Path: ox-prg!bowen >From: bowen@prg.ox.ac.uk (Jonathan Bowen) Newsgroups: comp.specification.z Subject: Re: Prove me wrong Message-ID: <1959@culhua.prg.ox.ac.uk> Date: 3 Jul 91 13:20:07 GMT References: <1991Jun28.175058.4987@agate.berkeley.edu> <2232@uqcspe.cs.uq.oz.au> <3919@sirius.ucs.adelaide.edu.au> Sender: news@prg.ox.ac.uk Reply-To: Jonathan.Bowen@prg.oxford.ac.uk (Jonathan Bowen) Organization: Programming Research Group, Oxford University, UK Lines: 40 In article <3919@sirius.ucs.adelaide.edu.au> tonyb@cs.adelaide.edu.au writes: >Is any of this stuff (oz.sty fuzz.sty) etc available through ftp >somewhere. Is any of the UQ stuff available electronically (as opposed >to snail mail) ? I'd love to get hold of it. Most of the UK is *still* not on Internet so there is no FTP access to such files as far as I know. :-( However, some are available via e-mail using the archive server at Oxford: LaTeX document preparation support: fuzz Order form for "fuzz" Z style for LaTeX + type-checker zed.sty A LaTeX style option for writing Z documents zguide.tex A guide to the above style oz.sty A LaTeX style option for writing Z & Object-Z documents oz.tex A guide to the above style threecolumn.sty A style option used by "oz.tex" (if you don't have it) foil.sty A LaTeX style for overhead projector foils zedfoil.sty A LaTeX style option for Z overhead projector foils foil.tex An example of using the above two style files Note that "fuzz" costs money but the rest are free. For detailed information on how to access the PRG archive server, send a message containing the command "help" to . Alternatively, send a command of "send z zed.sty zguide.tex" (for example) to the same address. The command "index z" will return a list of all the Z-related files on the server. If anyone is willing to make these (and other Z-related files) available via FTP, please contact me. Unfortunately we cannot afford direct Internet access at the moment. Alternatively, if anyone would like to send us a cheque ... :-) -- Jonathan Bowen, Oxford University Computing Laboratory. From ox-prg!ukc!mcsun!uunet!munnari.oz.au!bunyip.cc.uq.oz.au!uqcspe!cs.uq.oz.au!fmg Thu Jul 4 09:40:42 BST 1991 Status: O Article 28 of comp.specification.z: Path: ox-prg!ukc!mcsun!uunet!munnari.oz.au!bunyip.cc.uq.oz.au!uqcspe!cs.uq.oz.au!fmg >From: fmg@cs.uq.oz.au ( Formal Methods Group) Newsgroups: comp.specification.z Subject: Re: (none) Message-ID: <2280@uqcspe.cs.uq.oz.au> Date: 3 Jul 91 00:31:27 GMT References: <1991Jul2.160513.14254@software.org> Sender: news@cs.uq.oz.au Reply-To: fmg@cs.uq.oz.au Lines: 10 blakemor@software.org (Alex Blakemore) writes: >P.S. what is the email address of the "librarian" so people can >email rather than post requests ? the email address is fmg@cs.uq.oz.au if your news reader supports a reply command you should have no problems using that. Cheers, the fmg librarian. From ox-prg!dlb Thu Jul 4 09:43:49 BST 1991 Status: O Article 29 of comp.specification.z: Path: ox-prg!dlb >From: dlb@I2Wash.com (David Barton) Newsgroups: comp.specification.z Subject: Reasons for Participation Message-ID: <9107021608.AA07920@fanny.I2Wash.COM> Date: 2 Jul 91 16:08:36 GMT Sender: daemon@prg.ox.ac.uk Lines: 95 X-Mailer: mail-news 2.0.3 Participants in the Z forum: I joined this forum around the beginning of May, and in his welcoming message, Jonathan Bowen asked me to post a message to the list describing my own involvment with Z and the extent to which this work might effect the rest of the Z community. I have deliberately put this task off while I have read the various messages and tried to get the "feel" of the list and the Z community. I am now (finally) responding to Jonathan's request. My name is David Barton, and I work for Intermetrics, Inc. in the Washington, DC area. I have long had an interest in formal methods in computer science, and for this reason am delighted at the existence of Z and the Z community. I am trying hard to increase my knowledge about Z and related notations. For those of you in the hardware realm, my recent work has been connected with VHDL and related topics. My present work is divided into two areas: a related language called MHDL (for MIMIC Hardware Description Language), which is a language designed for the description of microwave and analog hardware, and a SDL (Systems Design Language) for the description of high level systems. The MHDL work is presently funded and under contract. The MHDL Working Group has just finished assembling (or is in the process of finally assembling) a requirements document for the language. The SDL work is proceeding under the auspices of the Design Automation Standards Subcommittee, under the Design Automation Technical Committee, under the Computer Society of the IEEE (how's that for a family tree?). The members of this committee are proceeding on a purely volunteer basis, with no funding at the present time. Funding may appear later in the process. The SDL working group is at present engaged in the creation of a requirements document for the SDL. My interests in Z and the capabilities of Z are connected with both activities. The requirements for MHDL call for an extremely flexible notation for defining microwave behavior, both in the form of functions and in the form of parameters which specify the behavior of generic devices to microwave engineers. These specifications must be composable at a very fine level of detail, and in a large variety of ways. The schema expressions of Z are the closest thing that I have been able to find to this general capability, and I am therefore extremely interested in the semantic definition of these expressions for use in MHDL. The connection with the SDL is more direct (if less urgent, as it is unfunded). Indeed, there is a strong argument to be made that Z is sufficient as a systems design language in itself. The discussions in my own working group indicate two areas in which the present Z syntax and semantics may not be sufficient. Both of these areas concern an ability that is not explicitly addressed by Z: the ability to describe a large system as an explicit network of communicating components (similar to CSP, but with more flexible communications mechanisms). Z can obviously describe such a situation; however, the syntax in which such a description would be couched is not immediately comprehensible to systems designers. In addition, components (nodes in the network) may be expressed in a multitude of notations, including but limited to; VHDL, MHDL, Ada, C++, and SDL. The need to incorporate specifications for these diverse notations has been addressed to an extent in the Z community in the brief time I have been reading this list, but not as explicitly as we would need. As the preceeding paragraph makes obvious, I am considerably hampered by my lack of knowledge. I am trying to fill in these gaps, and have various requests out via Email and to the various archive servers. I am posting this message both by way of introduction and as an appeal to those with similar interests to get in touch with me concerning these areas. Another interesting complication is the fact that both MHDL and SDL will eventually (in some form) become standards. MHDL will be released to some standards organization (probably the IEEE) upon completion of the language reference manual (LRM). The SDL working group is meeting under the DASS, which is a standards subcommittee. It is unclear to me what the best mechanism is for the SDL working group: if we should continue separately, incorporating part or all of Z; if we should join the Z standardization effort (about which I know next to nothing) and attempt to submit our issues there; or if some form of joining or cooperation is best. I am somewhat hesitant about how to approach the Z community, which is established and has its own agenda and needs, concerning these issues (and therefore, in the best American fashion, I just jump in with both feet by posting this note). I would be very glad indeed to hear any discussion or receive any comments concernining the connection between these two efforts. So much for my self-introduction. I hope I will be seen not as pushy or demanding, but as requesting enlightenment and clarification. I have enjoyed this list, and the responses from the various members have been courteous and informative. I hope that I may add to the discussions here. David Barton barton@i2wash.com From ox-prg!ukc!mcsun!cernvax!chx400!sicsun!disuns2!litsun9.epfl.ch!moreaux Thu Jul 4 09:44:50 BST 1991 Status: O Article 30 of comp.specification.z: Path: ox-prg!ukc!mcsun!cernvax!chx400!sicsun!disuns2!litsun9.epfl.ch!moreaux >From: moreaux@litsun9.epfl.ch (Michel Moreaux) Newsgroups: comp.specification.z Subject: Re: What is this group - HERE'S A GOOD INTRO. TEXT ON 'Z'... Message-ID: <2038@disuns2.epfl.ch> Date: 3 Jul 91 08:56:06 GMT References: <2161@uqcspe.cs.uq.oz.au> <7559@vela.acs.oakland.edu> Sender: news@disuns2.epfl.ch Lines: 32 Nntp-Posting-Host: litsun9.epfl.ch In article <7559@vela.acs.oakland.edu>, rdthomps@vela.acs.oakland.edu (Robert D. Thompson) writes: ] 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. I do not recommend this book because there are some unacceptable errors and lacks in the Z presentation part (lacks in accuracy in some Z schema's bodies where free symbols are used without beeing defined and typed). According to my opinion, this constitutes a paradoxal approach to the introduction of formal methods since one of the purpose of formal methods is to be accurate. I think that the following book gives a better introduction to the Z language : "Z an Introduction to Formal Methods", Antoni Diller, Wiley Ed., 1990. The book is easy to understand and clear. ------------------------------------------------------------------------------ Michel Moreaux, | "Ceux qui ne savent rien en savent Ecole Polytechnique Federale de Lausanne | toujours tout autant que ceux qui Departement d'Informatique | n'en savent pas plus qu'eux" Laboratoire d'Informatique Technique | P. Dac. EL-Ecublens |___________________________________ CH-1015 Lausanne Phone # : (21) 693-46-72, e-mail : moreaux@litsun.epfl.ch ------------------------------------------------------------------------------ From UNAUTHENTICATED Thu Jul 4 09:45:16 BST 1991 Status: O Article 31 of comp.specification.z: Path: ox-prg!ukc!mcsun!uunet!zaphod.mps.ohio-state.edu!ub!galileo.cc.rochester.edu!rochester!pt.cs.cmu.edu!o.gp.cs.cmu.edu!andrew.cmu.edu!+ >From: Paul.Kram@cs.cmu.edu Newsgroups: comp.specification.z Subject: Best Tool Message-ID: <4cQVYCq00h5KE9GVEo@cs.cmu.edu> Date: 3 Jul 91 18:35:58 GMT Organization: Carnegie Mellon, Pittsburgh, PA Lines: 11 Following the discusion of tools for writing Z specification (Latex etc.)... My favorite is pencil, paper and eraser. The adage "Be sure brain is in gear before engaging mouth" seems apropos to Z spec. writing. While this runs contrary to much "software engineering", I believe it is a timely break with tradition. The task of making "pretty specs" is second to the challenge of making pretty-good specs. From ox-prg!A.J.C.Blyth Thu Jul 4 09:45:34 BST 1991 Status: O Article 32 of comp.specification.z: Path: ox-prg!A.J.C.Blyth >From: A.J.C.Blyth@newcastle.ac.uk (A.J.C. Blyth) Newsgroups: comp.specification.z Subject: The Best Tool Message-ID: Date: 4 Jul 91 08:18:19 GMT Sender: news@prg.ox.ac.uk Lines: 8 X-Mailer: ELM [version 2.3 PL11] X-Mailer: mail-news 2.0.3 Following the discusion of tools for writing Z specification (Latex etc.)... I just thought that I would add my two penies worth I like and use the CADIZ tool. This tool uses troff to write Z, and it is nice and graphical and the raw troff text is readable. Andrew From UNAUTHENTICATED Thu Jul 4 11:30:22 BST 1991 Status: O Article 33 of comp.specification.z: Path: ox-prg!ukc!mcsun!uunet!zaphod.mps.ohio-state.edu!rpi!batcomputer!cornell!rochester!pt.cs.cmu.edu!o.gp.cs.cmu.edu!andrew.cmu.edu!+ >From: Paul.Kram@cs.cmu.edu Newsgroups: comp.specification.z Subject: DFDs vs. Z (was Re:Prove me wrong) Message-ID: Date: 3 Jul 91 19:32:42 GMT Organization: Carnegie Mellon, Pittsburgh, PA Lines: 28 DFD and Z each have their merits. The trick is knowing when, to use which, to say what, to whom. Ambiguity is helpful at early and intermediate stages of specification. A specifier needs to master a variety of expressions (including natural language). The large "market share" of DFDs can be partly explained by the relative newness of Z. DFDs have been popular for at least 15 years. Also, DFDs were developed in response to data-processing applications which are a large share of software development efforts. So... the number of people using a method (DFDs) is not a sound indication of the unfitness of an alternate method (Z). As my mother used to say, "Just because everyone else jumps off a bridge does not mean you should too." As to knowing when, to use which, to say what, to whom... If you know both, you'll know when to use which. As to explaining to clients, Object-Oriented Analysis (OOA) seems to be even better than DFD for some applications and I would check it out first if you don't know DFD or OOA. I suspect that DFD may be like COBOL in that it persists because of the large number of existing applications and trained people. Some say that OOA supersedes DFD. (I don't know.) I am unfamiliar with Object-Z. Does it compliment OOA? From ox-prg!alex Thu Jul 4 11:31:11 BST 1991 Status: O Article 34 of comp.specification.z: Path: ox-prg!alex >From: alex@minster.york.ac.uk Newsgroups: comp.specification.z Subject: Re: Removal from ZFORUM mail listing Message-ID: Date: 4 Jul 91 09:23:37 GMT Sender: daemon@prg.ox.ac.uk Lines: 4 X-Mailer: mail-news 2.0.3 Thank you for removing me from the Zforum. Alexandre Vasconcelos. From ox-prg!wang Thu Jul 4 11:31:32 BST 1991 Status: O Article 35 of comp.specification.z: Path: ox-prg!wang >From: wang@minster.york.ac.uk Newsgroups: comp.specification.z Subject: (none) Message-ID: Date: 4 Jul 91 09:26:33 GMT Sender: daemon@prg.ox.ac.uk Lines: 10 X-Mailer: mail-news 2.0.3 I like CADIZ too. It is powerful and easy to use! Bing |Following the discusion of tools for writing Z specification (Latex etc.)... |I just thought that I would add my two penies worth |I like and use the CADIZ tool. This tool uses troff to write Z, and |it is nice and graphical and the raw troff text is readable. |Andrew From ox-prg!macdonald%pyro.decnet Mon Jul 8 18:15:18 BST 1991 Article: 36 of comp.specification.z Path: ox-prg!macdonald%pyro.decnet From: macdonald%pyro.decnet@ccint1.rsre.mod.uk ("PYRO::MACDONALD") Newsgroups: comp.specification.z Subject: DFDs and Z Message-ID: <4346.9107041121@prg.oxford.ac.uk> Date: 5 Jul 91 05:58:17 GMT Sender: news@prg.ox.ac.uk Lines: 19 X-Mailer: mail-news 2.0.3 Status: O I agree with Paul Kram when he says: | DFD and Z each have their merits. The trick is knowing when, to use which, to | say what, to whom. (Indeed, work has been done on translating DFDs into outlines of Z specifications, and on extracting DFDs from Z specs: "Translating Data Flow Diagrams into Z (and Vice Versa)" GP Randell, RSRE Report 90019, October 1990.) However, he goes on to say: | Ambiguity is helpful at early and intermediate stages of specification. I hope he means non-determinism rather than ambiguity. Non-determinism is useful in specification, i.e. the specification leaves open a range of possible implementations, but it is clear what the possibilities are. Ambiguity, i.e. allowing different readers to interpret the same specification in different ways, is not helpful. From ox-prg!lrenshaw Mon Jul 8 18:15:49 BST 1991 Article: 37 of comp.specification.z Path: ox-prg!lrenshaw From: lrenshaw@axion.bt.co.uk (Laurence Renshaw) Newsgroups: comp.specification.z Subject: Re: The Best Tool Message-ID: <3658.9107041322@orion.axion.bt.co.uk> Date: 4 Jul 91 13:22:23 GMT Sender: news@prg.ox.ac.uk Lines: 21 X-Mailer: mail-news 2.0.3 Status: O A.J.C.Blyth@newcastle.ac.uk wrote : |Following the discusion of tools for writing Z specification (Latex etc.)... | |I just thought that I would add my two penies worth | |I like and use the CADIZ tool. This tool uses troff to write Z, and |it is nice and graphical and the raw troff text is readable. | |Andrew |From this description (and what I've seen of CADIZ), it doesn't sound like CADIZ is a tool for _writing_ Z at all. It's a tool for displaying and checking Z specs written using troff. Admittedly, CADIZ supplies macros for writing Z specs (like the FUZZ or OZ macros for LaTeX), but what people really seem to want (IMO) is a real editor - preferably WYSIWIG. I know that a few exist commercially - is it appropriate to discuss their merits on this mailing list/newsgroup ? Laurence Renshaw From ox-prg!timh Mon Jul 8 18:16:21 BST 1991 Article: 38 of comp.specification.z Path: ox-prg!timh From: timh@logcam.co.uk (Tim Hoverd) Newsgroups: comp.specification.z Subject: Thinly disguised adverts Message-ID: <1894.9107041307@jessica.logcam.co.uk> Date: 4 Jul 91 13:57:49 GMT Sender: news@prg.ox.ac.uk Lines: 12 In-Reply-To: wang@minster.york.ac.uk's message of Thu, 4 Jul 91 10:23:19 +0100 <16291.9107040923@prg.ox.ac.uk> X-Mailer: mail-news 2.0.3 Status: O | I like CADIZ too. It is powerful and easy to use! Please can we stop puffing our own tools and talk about Z instead? +--------------------------------+---------------------------------+ |Tim Hoverd |Phone: +44 223 66343 | |Logica Cambridge Limited | | |Betjeman House |UUCP : timh@logcam.co.uk | |104 Hills Road | timh@logcam.uucp | |Cambridge CB2 1LQ | ...!mcvax!ukc!logcam!timh | +--------------------------------+---------------------------------+ From ox-prg!ukc!mcsun!unido!math.fu-berlin.de!ira.uka.de!sol.ctr.columbia.edu!samsung!uunet!munnari.oz.au!bunyip.cc.uq.oz.au!uqcspe!cs.uq.oz.au!thomo Mon Jul 8 18:16:58 BST 1991 Article: 39 of comp.specification.z Path: ox-prg!ukc!mcsun!unido!math.fu-berlin.de!ira.uka.de!sol.ctr.columbia.edu!samsung!uunet!munnari.oz.au!bunyip.cc.uq.oz.au!uqcspe!cs.uq.oz.au!thomo From: thomo@cs.uq.oz.au (John Thomas) Newsgroups: comp.specification.z Subject: Re: What is this group (was Test) Message-ID: <2187@uqcspe.cs.uq.oz.au> Date: 27 Jun 91 11:14:43 GMT References: <2161@uqcspe.cs.uq.oz.au> <1991Jun27.042414.7381@mlb.semi.harris.com> Sender: rootksh@cs.uq.oz.au Reply-To: thomo@cs.uq.oz.au Lines: 23 Status: O In <1991Jun27.042414.7381@mlb.semi.harris.com> john@mintaka.mlb.semi.harris.com (John M. Blasik) writes: [lots deleted] >standardization. Comp.specification.z would provide a convenient forum >for messages concerned with recent developments and the use of Z. Just to get the proverbial ball rolling.... What are your ("your" as in you people reading this group) opinions wrt object-Z IMHO it beats the heck out of plain vanilla 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 ! | +------------------+ *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-* From ox-prg!ukc!warwick!covpoly!cck.cov.ac.uk!unreplyable!garbage Mon Jul 8 18:18:05 BST 1991 Article: 40 of comp.specification.z Path: ox-prg!ukc!warwick!covpoly!cck.cov.ac.uk!unreplyable!garbage From: csx040@cck.cov.ac.uk (Alan Chantler (CS)) Newsgroups: comp.specification.z Subject: Re: Prove me wrong Message-ID: Date: 4 Jul 91 08:16:57 GMT References: <1991Jun28.175058.4987@agate.berkeley.edu> <1991Jul2.105231.20473@fmg.bt.co.uk> Organization: Coventry Polytechnic, Coventry, UK Lines: 44 Status: O In article <1991Jul2.105231.20473@fmg.bt.co.uk> jcrw@fmg.bt.co.uk (Jeremy Wilson) writes: > >What is perhaps more to the point is whether Z and DFD's do the same job. >As far as I can understand DFD's are essentially an informal graphical > descriptive technique. Their main beauty is that they are understandable >(supposedly) to the customer. There are, however, many functional aspects > of a system which are not described. In most so-called "methodologies" DFD's > are supplemented by a plethora of other "notations", eg ERD's ELH's > Nasi-Schnurliman (my apologies to the relevant inventors if I got their names Nassi-Schneiderman >wrong) diagrams , etc etc etc. > > >There may well a good argument for using DFD's and other graphical notations > in conjunction with formal languages. Has anyone any thoughts about this? > Yes, I do. It is my opinion that ALL methodologies have their place in the scheme of things. What I try to do is to bring as many as possible to the attebtion of practitioners and let them make up their own minds which is best for their purposes. Z is notoriously non-graphic, and many people have some difficulty in appreciating the imediate value of a formally specified description. The combined use of diagrammatic methods with the proper (rigorous) usage of Z can help to ensure that all parties to the development of a specification can keep up with it. Obviously all self-respecting systems developers will involve the user (customer) at all stages. The use of a formal notation reduces possible ambiguities but can cause confusion to those not mathematically developed! Even the effective use of a 'Z Document' as described by Spivey (including the simultaneous development of the Z and plain-text descriptions) may not be sufficiently clear without the support of some diagrams. -- AlanC@coventry.ac.uk | Post: Coventry Polytechnic JANET: AlanC@uk.ac.coventry | Priory Street INET : AlanC%coventry.ac.uk@nsfnet-relay.ac.uk | Coventry, UK Phone: +44 203 838332 | CV1 5FB From ox-prg!ukc!mcsun!uunet!zaphod.mps.ohio-state.edu!samsung!munnari.oz.au!metro!otc!karenr Mon Jul 8 18:18:35 BST 1991 Article: 41 of comp.specification.z Path: ox-prg!ukc!mcsun!uunet!zaphod.mps.ohio-state.edu!samsung!munnari.oz.au!metro!otc!karenr From: karenr@otca.oz.au (Karen Rosenberg) Newsgroups: comp.specification.z Subject: FDTs and Graphical Notations (was Re: Prove me wrong) Message-ID: Date: 4 Jul 91 23:35:51 GMT References: <1991Jun28.175058.4987@agate.berkeley.edu> <1991Jul2.105231.20473@fmg.bt.co.uk> Sender: news@otc.otca.oz Organization: OTC Development Unit, Australia Lines: 38 In-reply-to: jcrw@fmg.bt.co.uk's message of 2 Jul 91 10:52:31 GMT Status: O In article <1991Jul2.105231.20473@fmg.bt.co.uk> jcrw@fmg.bt.co.uk (Jeremy Wilson) writes: There may well a good argument for using DFD's and other graphical notations in conjunction with formal languages. Has anyone any thoughts about this? I agree with this wholeheartedly. Neither formal description techniques or more conventional graphical notations, e.g. DFDs, ERDs, etc., can by themselves completely model a system in a way that will be totally understandable by users/customers. Formal techniques have the advantage that they can completely model a system in a rigorous, correct manner. However, many customers out there do not come from a mathematical or computing background, so will find it difficult to understand such specifications. The use of a diagramming technique along the lines of DFDs or ERDs can act as an "interface" to the more complete formal specification. In a sense, the diagrams would guide the reader through the formal specification. It may be difficult, however, to integrate a particular diagramming technique and formal description technique. A related possibility is that a formal description technique may be able to act as a "backbone" reference for the variety of techniques used and diagrams produced during the different phases of software development. For example, a particular class in Object-Z will contain a state and operations on that state. The state part will correspond to an ERD whereas the operations "may" correspond to a DRD. It remains to be seen how well this would work. Has anyone else any thoughts on these ideas? -- Karen Rosenberg |||| OTC || ACSnet: karenr@otc.otca.oz.au UUCP: {uunet,mcvax}!munnari!otc!karenr Snail: GPO Box 7000, Sydney 2001, Australia Voice: +61 2 287 3157 Fax: +61 2 287 3299 From ox-prg!draper%bigwig Mon Jul 8 18:19:23 BST 1991 Article: 42 of comp.specification.z Path: ox-prg!draper%bigwig From: draper%bigwig@rrl.uucp (draper) Newsgroups: comp.specification.z Subject: Refinement of specifications Message-ID: <9107050802.AA28904@bigwig.research> Date: 5 Jul 91 08:02:30 GMT Sender: daemon@prg.ox.ac.uk Lines: 36 X-Mailer: mail-news 2.0.3 Status: O I have been thinking about how to approach refinement of a Z specification. The sort of specification I have in mind starts off with a number of type schemas, which are used to define a system schema. The required operations are defined to act on the system schema. As an example, I may be specifying a cash dispenser. One of the components is: accounts: AccNo -> Account where Account is a schema type, and has a component mapping Cards (another schema) to PINs. The data refinements I have seen all work on a single type schema. When I'm refining a specification, what I really want to do is to be able to do a data refinement on the constituent types or components and then use these to get a concrete system schema. Ideally I would be able to use the abstraction function from the data refinement to calculate concrete versions of the system operations. So what I want to do is to refine my representation of the Account type, then refine my representation of the accounts component, and then (combining it with other refined components) the whole cashpoint. The problem I forsee is that the required operations on each component are not defined explicitly, so I can't check the refinement for applicability and correctness (until I get to the system level). Of course I could adopt an object-oriented style and define all of the operations on the components, but thatjust gives me more proof obligations and I don't want to anyway. Am I looking at this in a sensible way? If so, what constraints do I need on the data refinements to let me combine them, and how do I do it? Christine Draper Racal Research From ox-prg!INFSLESLEY Mon Jul 8 18:20:15 BST 1991 Article: 43 of comp.specification.z Path: ox-prg!INFSLESLEY From: INFSLESLEY@PRIMEB.LEEDS-POLY.AC.UK ("Lesley Semmens") Newsgroups: comp.specification.z Subject: (none) Message-ID: <12006.9107051027@prg.oxford.ac.uk> Date: 5 Jul 91 19:28:15 GMT Sender: daemon@prg.ox.ac.uk Lines: 39 X-Mailer: mail-news 2.0.3 Status: O Re: DFDs and Z I have been working on the integration of Yourdon and Z, this involves using Yourdon for the initial system specification and then translating the Yourdon ERD and DFD diagrams (plus appropriate Data Dictionary entries) into Z. This process gives the system state and skeleton operation schemas. The operation schemas are then completed with pre- and post-conditions equivalent to those which would have formed Yourdon pspecs (mini specifications). We have done a couple of small case studies and a group of post-graduate students at Sheffield are using the integrated method to develop a Flexi-Time system ... we hope to submit the results of this last study for publication, after its completion in August. A paper on the early stages of the work, by myself and Pat Allen, was presented at the Fifth Annual Z User Meeting, the proceedings of which are to be published soon in the Springer-Verlag _Workshops in Computing_ series. A paper formalising the relationship between the diagrams and Z is to be presented at a Methods Integration workshop/one-day conference, here in Leeds, in September. Apart from our own work, there is much interest in the integration of structured methods (which include graphical notations) and formal notations. Academic projects in Europe include SAZ: SSADM (British Govenment mandated method) and Z, at York University; and work on Yourdon and VDM at Delft University of Technology, Netherlands. British Aerospace use CORE (Controlled Requirements Expression) and Z; Rolls Royce and Associates use VDM with Yourdon; Bull, Paris are working on using IDE's Software Through Pictures and VDM; and some at IBM (Hursley Park) use DFDs as an addition to the explanatory English text in Z documents. Lesley Semmens Faculty of Information and Engineering Systems Leeds Polytechnic The Grange Beckett Park Leeds LS6 3QS From ox-prg!dc Mon Jul 8 18:20:46 BST 1991 Article: 44 of comp.specification.z Path: ox-prg!dc From: dc@cs.warwick.ac.uk (Douglas Chester) Newsgroups: comp.specification.z Subject: Obj-Orien. Z, was: HERE'S A GOOD INTRO. TEXT Message-ID: <3143.9107051224@slate.warwick.ac.uk> Date: 5 Jul 91 12:24:48 GMT Sender: daemon@prg.ox.ac.uk Lines: 14 X-Mailer: mail-news 2.0.3 Status: O | 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: I would be interested in a copy of the Object-z reference manual. Thanks. Douglas Chester Department of Computer Science University of Warwick Coventry CV4 7AL dc@uk.ac.warwick.cs From ox-prg!DC_INCE Mon Jul 8 18:22:03 BST 1991 Article: 45 of comp.specification.z Path: ox-prg!DC_INCE From: DC_INCE@VAX.ACS.OPEN.AC.UK Newsgroups: comp.specification.z Subject: The possible lack of popularity of Z in the industry Message-ID: <13946.9107051412@prg.oxford.ac.uk> Date: 5 Jul 91 14:11:43 GMT Sender: daemon@prg.ox.ac.uk Lines: 47 X-Mailer: mail-news 2.0.3 Status: O The recent correspondence about data flow diagrams has prompted me to write this note. Please don't imagine this is a publicity blurb but in a book which is to be published in September the authors show how both data flow diagrams structure charts and VDM --- the greatest formal method in the history of the world -- can be combined together. The book is Practical Formal Methods with VDM D Andrews and D Ince, Mcgraw-Hill On another tack. The last two years I have visited a number of companies and given a series of public seminars to staff in the software industry At the beginning of the seminars I carry out a straw poll of the staff who are mainly at the position where they are able to look down globally in a company and accurately answer these questions. I must have spoken to staff from about 200 companies and yet I have only found one using using formal methods (VDM)in anger the range of companies I meet is wide from safety critical companies to commercial data processing . Another interesting statistic is that only 3% had ever heard of formal methods. There are a wide variety of reasons for this. Here are some: * I have been speaking to the wrong people. * The formal methods community is particulalry bad at communicating the advantages of formal methods * Until recently there has been a shortage of good teaching materials * The conservatism of British industry. (Sorry America and other European countries I ahve no experience of industrial practice in these countries) * That for the vast majority of comapnies graphical techniques such as Yourdon are adequate * There are a lot of purists in the formal methods community who are first, unable to communicate with the industry and, second, do not realise that change comes incrementally in information technology not in a big bang fashion. * The lack of tools as compared with less formal methods. From ox-prg!DC_INCE Mon Jul 8 18:22:44 BST 1991 Article: 46 of comp.specification.z Path: ox-prg!DC_INCE From: DC_INCE@VAX.ACS.OPEN.AC.UK Newsgroups: comp.specification.z Subject: Z Book Message-ID: <14200.9107051442@prg.oxford.ac.uk> Date: 5 Jul 91 14:41:43 GMT Sender: daemon@prg.ox.ac.uk Lines: 18 X-Mailer: mail-news 2.0.3 Status: O I notice from my email that there was a message from someone in France about my Z book being slightly critical about it I would like to ask people generally what they think about the book, for two reasons. First, the criticisms do not match the feedback that OUP have received about the book in terms of reviews and the cards that are sent out eliciting lecturers views. Second, I am about to start a second edition. I am happy to take criticism over email no matter how harsh. I take the view that any criticism will improve the second edition. To the French correspondent who sent the orginal email could I have some page references. If there are any problems then assuming they are not the product of purist cant I will fix them up in the second edition. From ox-prg!wang Mon Jul 8 18:22:51 BST 1991 Article: 47 of comp.specification.z Path: ox-prg!wang From: wang@minster.york.ac.uk Newsgroups: comp.specification.z Subject: (none) Message-ID: Date: 5 Jul 91 14:56:13 GMT Sender: daemon@prg.ox.ac.uk Lines: 19 X-Mailer: mail-news 2.0.3 Status: O | 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: I'd be interested in a copy of the Object-z reference manual too. Many thanks in advance! +--------------------------+-----------------------------------------------+ |Bing Wang |JANET: wang@uk.ac.york.minster |Dept. of Computer Science |EARN: wang@minster.york.ac.uk |University of York |UUNET: ..!uunet!mcsun!ukc!minster!wang |York YO1 5DD ENGLAND |ARPA: wang%york.minster@nfsnet-relay.ac.uk | |INTERNET: wang%minster.york.ac.uk@nsfnet-relay.ac.uk |Tel: (0904) 432710 | | (+44 0904) 432710 | | +--------------------------+-----------------------------------------------+ From ox-prg!sean Mon Jul 8 18:23:42 BST 1991 Article: 48 of comp.specification.z Path: ox-prg!sean From: sean@aipna.ed.ac.uk Newsgroups: comp.specification.z Subject: Re: asking for the Object Z manual. Message-ID: <17337.9107051842@affric.aipna.ed.ac.uk> Date: 5 Jul 91 18:42:45 GMT Sender: daemon@prg.ox.ac.uk Lines: 35 X-Mailer: mail-news 2.0.3 Status: O This must be about the tenth or so identical, content free message that has arrived in my mailbox in the last few days. | 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 lib rarian | at the Department of Computer Science, University of Queensland: I'd be interested in a copy of the Object-z reference manual too. Many thanks in advance! I am sure that the people in Queensland are all truely thrilled to see how many people want to know about their system, but the rest of us are truely pissed off that there are so many people out there who either cannot read a simple mail message or are incompetent to use a mailer properly. If you want the manual, then get in touch with the librarian, like it says in the message. DO NOT BOTHER THE REST OF US, WHO HAVE BETTER THINGS TO DO THAN BE DISTRACTED BY THE ENTHUSIASTIC COMPUTER ILLITERATES WHO SEEM TO FILL COMPUTER SCIENCE DEPARTMENTS Sean Sean Matthews 80 South Bridge, Edinburgh, UK Dept. of Artificial Intelligence +44 (0) 31 650 2722 University of Edinburgh sean@castle.ed.ac.uk From ox-prg!Thomas.McGinnis Mon Jul 8 18:25:35 BST 1991 Article: 49 of comp.specification.z Path: ox-prg!Thomas.McGinnis From: Thomas.McGinnis@TR4.GP.CS.CMU.edu Newsgroups: comp.specification.z Subject: Generics Question for Soar 6 specification Message-ID: <16746.678739287@TR4.GP.CS.CMU.EDU> Date: 5 Jul 91 18:41:27 GMT Sender: daemon@prg.ox.ac.uk Lines: 93 X-Mailer: mail-news 2.0.3 Status: O Specifiers, Hi, I'm Brian Milnes. I'm on staff here at the School of Computer Science at Carnegie Mellon University. I work for Allen Newell on the Soar project. Soar is a cognitive architecture designed to be both an exemplar Unified Theory of Cognition and an architecture for artificial intelligence. We are specifying, designing and implementing the next version of Soar, Soar 6. We did not intend to produce a formal specification of Soar, but an initial attempt to formalize a small component of the system produced such a clear view of that component that we launched into a formal specification. However, foolishly we did not start out by scouring the literature for the array of fine specification languages available, until last fall. After a search, we chose Z. The specification has been most helpful in clarifying a quite murky system, and I have about a 45 page specification of straight Z. It's about 75% complete, and will stillrequire several man months to finish. On to my question, I'm having difficulty with a limitation of generics. In several different places we have a "concept" that I would like to represent as a function (or relation) that applies over a hierarchy of data types. I am attempting to use generics but the grammar for Z (and fuzz) is restrictive about how I can use them. Soar has a production system as a component (that models long term memory/short term memory). In describing this system, I have a hierarchy of data such as: Value || \/ - means test includes Values in its definition. Test || \/ PreferenceType[T1,T2] || \/ Condition Two values are connected under certain conditions, two tests are connected on conditions based upon the connection of their values, and so on up to conditions. To describe this I build one generic relation, connected[Type] where type should range over Value, Test, PreferenceTest and Condition. I then would like to write generic definitions containing the axioms for each type instantiated version of connected. For example, \begin{gendef}[T] Connected : T \rel T \end{gendef} \begin{zed} \forall v_1, v_2 : Value @ Connected(v_1,v_2) \iff \ldots \end{zed} This works fine until I need to parameterize over my PreferenceType. As value is a base type, I need no parameters but when I try and install them in PreferenceType, I discover that the Decl-Part is not optional. \begin{gendef}[T1,T2] \where \forall p_1,p_2 : PreferenceType[T1,T2] @ \\ Connected(p_1,p_2) \iff \ldots \end{gendef} The question: What is an elegant way to do this ? I could define "ConnectedValues", "ConnectedTests", "Connected..." but this adds quite a lot of verbiage to an already lengthy specification. Also, I actually use this definition style in about five places. Is there some particular semantic reason that a generic definition must have an axiom part and a declaration part ? Fuzz does certainly not check that the axiom part mentions anything declared in the decl-part anyway. Thanks, Brian P.S. I also have other difficulties with Z, most notably how to use Z to specify control flow. I'll ponder those questions for you sometime else. From ox-prg!ukc!newcastle.ac.uk!ugle!najcb Mon Jul 8 18:25:59 BST 1991 Article: 50 of comp.specification.z Path: ox-prg!ukc!newcastle.ac.uk!ugle!najcb From: A.J.C.Blyth@newcastle.ac.uk (A.J.C. Blyth) Newsgroups: comp.specification.z Subject: Tools for Z Keywords: Z Tools Message-ID: <1991Jul5.083623.18825@newcastle.ac.uk> Date: 5 Jul 91 08:36:23 GMT References: <1894.9107041307@jessica.logcam.co.uk> Sender: news@newcastle.ac.uk Organization: Computing Laboratory, U of Newcastle upon Tyne, UK NE17RU Lines: 13 Status: O In article <1894.9107041307@jessica.logcam.co.uk>, timh@logcam.co.uk (Tim Hoverd) writes: |> | I like CADIZ too. It is powerful and easy to use! |> |> Please can we stop puffing our own tools and talk about Z instead? |> I think that the current state of tools that manipulate Z is a subject worthy of discussion on this group. By that I do not mean adverts, but peoples honest opinions of that the want out of a tool and what the current tools do or non't give you. Andrew From UNAUTHENTICATED Mon Jul 8 18:26:33 BST 1991 Article: 51 of comp.specification.z Path: ox-prg!ukc!mcsun!uunet!elroy.jpl.nasa.gov!ncar!hsdndev!rutgers!rochester!pt.cs.cmu.edu!o.gp.cs.cmu.edu!andrew.cmu.edu!+ From: Paul.Kram@cs.cmu.edu Newsgroups: comp.specification.z Subject: Re: DFDs and Z Message-ID: Date: 6 Jul 91 22:03:59 GMT Organization: Carnegie Mellon, Pittsburgh, PA Lines: 26 Status: O PYRO says: >> | Ambiguity is helpful at early and intermediate stages of specification. I hope he means non-determinism rather than ambiguity. Non-determinism is useful in specification, i.e. the specification leaves open a range of possible implementations, but it is clear what the possibilities are. Ambiguity, i.e. allowing different readers to interpret the same specification in different ways, is not helpful. << I was thinking that a certain amount of hand-waving can be useful when trying to ferret out user-requirements from clients. High- level DFDs (without a data-dictionary) can be vague and ambiguous because the semantics of the diagrams are not precisely defined. Nonetheless, they provide a framework for a client-user to give you more precise information. The ambiguities can raise important questions and prompt users to talk. I assume a good deal of client-user interaction in the early and intermediate stages of specification and how well a specification language supports this dialog is an important consideration. Others have commented on the difficulty of introducing Z-specifications to the mathmatically deprived. From ox-prg!wallace Mon Jul 8 18:27:34 BST 1991 Article: 52 of comp.specification.z Path: ox-prg!wallace From: wallace@cookie.enet.dec.com (06-Jul-1991 1134) Newsgroups: comp.specification.z Subject: ASCII Z symbols Message-ID: <9107061731.AA01544@enet-gw.pa.dec.com> Date: 6 Jul 91 17:31:02 GMT Sender: news@prg.ox.ac.uk Lines: 165 X-Mailer: mail-news 2.0.3 Status: O Someone asked for ASCII equivalents in this newsgroup. Here are the ones that a few of us at Digital Equipment Corp. have cooked up. The point that with X-terminals and the amount of font foundry software out there the need for this type of thing only really applies to things *like* the transmission medium of this newsgroup (a.k.a. 7-bit ASCII). =========================================================================== Richard Wallace Digital Equipment Corp CXN1/4 1175 Chapel Hills Dr. Colorado Springs, CO 80920 =========================================================================== ASCII Character Equivalents for Graphic Z Symbols ------------------------------------------------- The pp[xx] following the rightmost ASCII definition are the page numbers in the Z reference manual that define the symbol. This ASCII table is a translation of the table on page 150 of J.M. Spivey's "The Z Notation, a reference manual" Each ASCII representation is chosen for its lexical similarity to the actual Z symbol. In the case of the "<" letter ">" ASCII symbol, it was felt that this was the clearest di-tri-quadgraph to impart the meaning of the original symbol. All symbol equivalents are separated by "white space" with no "white space" allowed withing the di-tri-quadgraph. Power Set

(case sensitive) pp27,59 Cartisian Product (case sensitive) pp27,59 Schema Type <|| . . .||> pp28 Schema Definition, horizontal ^= (order specific) pp51 Abbreviated definition == (same) pp52,79 Tuple (...) (same) pp58 Set Display {...} (same) pp58,60 Lambda Expression (case sensitive) pp61 Mu Expression (case sensitive) pp61 Selection . (same) pp63 Binding Formation (case sensitive) pp64 Sequence of Elements <<...>> pp67 Bag of Elements [|...|] pp67 Equality = (same) pp69 Membership (case sensitive) pp69 Non-membership (case, order specific) pp89 Negation /- (order specific) pp70,75 Conjunction /\ pp70,75 Disjunction \/ pp70,75 Implication ==> pp70,75 Equivalence <=> pp70,75 Universal Quantifier (case sensitive) pp71,76 Existential Quantifier (case sensitive) pp71,76 Schema Hiding \ (same) pp76 Schema Projection <|`> (order specific) pp76 Filtering <|`> pp122 Sequential Composition <;> pp77,136 Inequality /= pp89 Empty Set {} pp90 Subset Relation (case, order sensitive) pp90 Proper Subset Relation (case sensitive) pp90 Non-empty Subsets (case, order sensitive) pp90 Set Union (case sensitive) pp91 Set Intersection (case sensitive) pp91 Binary Relations <-> pp95 Maplet |-> pp95 Backward Relational Composition (case sensitive) pp97 Domain Restriction <| pp98 Range Restriction |> pp98 Domain Anti-Restriction /<| pp99 Range Anti-Restriction /|> pp99 Relational Inversion R^~ (where "R" is the relation) pp100 Relational Image (| . . . |) pp101 Transitive Closure R^+ (where "R" is a relation) pp102 Reflexive-Trasitive Closure R^* (where "R" is a relation) pp102 Partial Functions +-> pp105 Total Functions --> pp105 Partial Injections >+> pp106 Total Injections >-> pp106 Partial Surjections +->> pp107 Total Surjections -->> pp107 Bijections >->> pp107 Functional Overriding (+) pp108 Natural Numbers (case sensitive) pp110 Strictly Positive Integers (case sensitive) pp111 Integers (case sensitive) pp110 Iteration R^(k) (parenthesis required) pp112 Number Range .. (same) pp113 Finite Sets (case sensitive) pp114 Non-empty Finite Sets (case sensitive) pp114 Number of members in a set # (same) pp114 Finite Partial Functions -++> pp115 Finite Partial Injections >++> pp115 Distributed Concatenation ^/ pp124 Concatenation ^^ pp119 Bag Union (order, case sensitive) pp128 Set Comprehension <*> pp60 Change in state of schema (case sensitive) pp134 Access with no change in state (order, case sensitive) pp134 of schema Unique Quantifier (order, case sensitive) pp32 From ox-prg!ukc!mcsun!uunet!bellcore!porthos!taichi!haim Mon Jul 8 18:28:33 BST 1991 Article: 53 of comp.specification.z Path: ox-prg!ukc!mcsun!uunet!bellcore!porthos!taichi!haim From: haim@taichi.uucp (24122-Haim Kilov(L028)m000) Newsgroups: comp.specification.z Subject: Re: FDTs and Graphical Notations (was Re: Prove me wrong) Message-ID: <1991Jul5.145042.8664@porthos.cc.bellcore.com> Date: 5 Jul 91 14:50:42 GMT References: <1991Jul2.105231.20473@fmg.bt.co.uk> Sender: netnews@porthos.cc.bellcore.com (USENET System Software) Reply-To: haim@taichi.UUCP (24122-Haim Kilov) Organization: Bellcore, Livingston, NJ Lines: 58 Status: O In article karenr@otca.oz.au (Karen Rosenberg) writes: ... >Formal techniques have the advantage that they can completely model a >system in a rigorous, correct manner. However, many customers out there do >not come from a mathematical or computing background, so will find it >difficult to understand such specifications. The use of a diagramming >technique along the lines of DFDs or ERDs can act as an "interface" to the >more complete formal specification. In a sense, the diagrams would guide >the reader through the formal specification. > >It may be difficult, however, to integrate a particular diagramming >technique and formal description technique. A related possibility is that >a formal description technique may be able to act as a "backbone" reference >for the variety of techniques used and diagrams produced during the >different phases of software development. For example, a particular class >in Object-Z will contain a state and operations on that state. The state >part will correspond to an ERD whereas the operations "may" correspond to a >DRD. It remains to be seen how well this would work. > >Has anyone else any thoughts on these ideas? > >-- > Karen Rosenberg > |||| OTC || > > ACSnet: karenr@otc.otca.oz.au > UUCP: {uunet,mcvax}!munnari!otc!karenr > Snail: GPO Box 7000, Sydney 2001, Australia > Voice: +61 2 287 3157 > Fax: +61 2 287 3299 I agree with the "guidance" idea. However, the guides may be incomplete and sometimes even misleading (to quote Bertrand Meyer, "try to find seven errors in a picture"). They should be used with care. On the last paragraph, it is not so easy to agree. ERD represent MORE than just "state part": by means of defining a thing as a relationship, or a weak entity, or a composite entity, or ..., important behavioral (CRUD) properties of this thing and associated things are defined. Therefore at least some generic operations for the thing are defined. For instance, if a thing X is defined as a weak entity with respect to thing Y then a precondition for creating an instance of X is defined: an appropriate instance of Y should exist. By the same token, a postcondition for deleting an instance of Y is defined: all appropriate instances of X will cease to exist. And an invariant is defined: the existence of an instance of X implies the existence of an instance of Y. No "DFD" is needed for this purpose (and the "data" do not "flow", anyway). I have published a paper on these topics in TOOLS'91: Generic information modeling concepts: a reusable component library, by H.Kilov, Proc. TOOLS'91 (ed. by B.Meyer and J.Bezivin), Prentice-Hall, 1991. Hope this helps. -Haim Kilov haim@bcr.cc.bellcore.com From ox-prg!ukc!mcsun!uunet!elroy.jpl.nasa.gov!sdd.hp.com!uakari.primate.wisc.edu!zaphod.mps.ohio-state.edu!hobbes.physics.uiowa.edu!news.iastate.edu!vaxf.iastate.edu!TAAK9 Mon Jul 8 18:29:30 BST 1991 Article: 54 of comp.specification.z Path: ox-prg!ukc!mcsun!uunet!elroy.jpl.nasa.gov!sdd.hp.com!uakari.primate.wisc.edu!zaphod.mps.ohio-state.edu!hobbes.physics.uiowa.edu!news.iastate.edu!vaxf.iastate.edu!TAAK9 From: taak9@isuvax.iastate.edu (Steve Sheldon) Newsgroups: comp.specification.z Subject: Re: The possible lack of popularity of Z in the industry Message-ID: <1991Jul5.165631.823@news.iastate.edu> Date: 5 Jul 91 16:56:31 GMT References: <13946.9107051412@prg.oxford.ac.uk> Sender: news@news.iastate.edu (USENET News System) Reply-To: taak9@isuvax.iastate.edu Organization: Iowa State University, Ames, IA. Lines: 35 Status: O In article <13946.9107051412@prg.oxford.ac.uk>, DC_INCE@VAX.ACS.OPEN.AC.UK writes: >... >Another interesting statistic is that only 3% had ever heard of >formal methods. There are a wide variety of reasons for this. > Here are some: > >* I have been speaking to the wrong people. > >* The formal methods community is particulalry bad at communicating the >advantages of formal methods > >* Until recently there has been a shortage of good teaching materials I've been reading this group hoping to get some better idea of what Z is, and a better idea of what formal specifications are. I recently had the overwhelming joy of taking a class in Software Engineering, where we were supposedly going to learn all about specifications and the design process. I don't recall learning anything of any particular use, just a bunch of academic theory. Well, after this experience, I have to agree with the last two arguments above why few individuals use these tools. The teaching materials used in our class explained nothing. And it was the general opinion of my project group that we would have been a heck of a lot better off specifying our design in plain simple english, possibly with FOPC to explain some points further. Our spec would have been easier to write, and certainly easier to read, thus there were no advantages, just signifigant disadvantages. Steve Sheldon taak9@ccvax.iastate.edu Computer Science undergrad Iowa State University From ox-prg!ukc!mcsun!uunet!wuarchive!mit-eddie!micro-heart-of-gold.mit.edu!uhog!jbs Mon Jul 8 18:30:00 BST 1991 Article: 55 of comp.specification.z Path: ox-prg!ukc!mcsun!uunet!wuarchive!mit-eddie!micro-heart-of-gold.mit.edu!uhog!jbs From: jbs@fenchurch.fenchurch.mit.edu (Jeffrey Siegal) Newsgroups: comp.specification.z Subject: What is Z? Message-ID: Date: 6 Jul 91 19:44:11 GMT Sender: news@micro-heart-of-gold.mit.edu (USENET News System) Organization: /u/jbs/.organization Lines: 3 Nntp-Posting-Host: fenchurch.mit.edu Status: O Please reply by mail. Jeffrey Siegal From ox-prg!prg.ox.ac.uk!zforum-request Mon Jul 8 18:30:27 BST 1991 Article: 56 of comp.specification.z Path: ox-prg!prg.ox.ac.uk!zforum-request From: zforum-request@prg.oxford.ac.uk Newsgroups: comp.specification.z Subject: Monthly comp.specification.z message Message-ID: <1975@culhua.prg.ox.ac.uk> Date: 7 Jul 91 22:59:45 GMT Sender: news@prg.ox.ac.uk Organization: Programming Research Group, Oxford University, UK Lines: 69 Status: O ************************* * MONTHLY MESSAGE * ************************* NAME: comp.specification.z STATUS: unmoderated PURPOSE: Discussion concerning the formal specification notation Z. 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 BSI standardization in the UK. Comp.specification.z provides a convenient forum for messages concerned with recent developments and the use of Z. Electronic mailing list: There is an associated Z FORUM mailing list. Articles are automatically cross-posted between comp.specification.z and the mailing list for those whose do not have access to USENET news. This may apply particularly to industrial Z users who are particularly encouraged to subscribe and post their experiences to the list. Contact with your name, address and e-mail address to join the mailing list. Messages for submission to the Z FORUM mailing list and the comp.specification.z newsgroup may be e-mailed to . Postal mailing list: If you wish to join the postal Z mailing list, please send your address to the industrial liaison secretary at the PRG in Oxford on . This will ensure you receive details of Z meetings, etc., particularly for people without access to electronic mail. 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 annual Z User Meetings held each December. 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 for further information on how to use the server. If anyone can provide FTP access to these files, please contact . 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 . Meetings: VDM'91 will be held on 21-25 October 1991, at Delft, the Netherlands. The meeting will include papers on Z. For further information, please e-mail the command "send z vdm91" to the PRG archive server. The 6th annual Z User Meeting will be held on 16-17 December 1991, at York University, England. Details will be distributed via comp.specification.z and Z FORUM. If you would like brief details of any other forthcoming Z-related meetings included here, please contact . This message was last updated on 3rd July 1991. -- Jonathan Bowen, Programming Research Group, Oxford University Computing Laboratory, UK. From ox-prg!prg.ox.ac.uk!zforum-request Mon Jul 8 18:30:45 BST 1991 Article: 57 of comp.specification.z Path: ox-prg!prg.ox.ac.uk!zforum-request From: zforum-request@prg.oxford.ac.uk Newsgroups: comp.specification.z Subject: Monthly comp.specification.z message Message-ID: <1976@culhua.prg.ox.ac.uk> Date: 7 Jul 91 23:00:22 GMT Sender: news@prg.ox.ac.uk Organization: Programming Research Group, Oxford University, UK Lines: 69 Status: O ************************* * MONTHLY MESSAGE * ************************* NAME: comp.specification.z STATUS: unmoderated PURPOSE: Discussion concerning the formal specification notation Z. 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 BSI standardization in the UK. Comp.specification.z provides a convenient forum for messages concerned with recent developments and the use of Z. Electronic mailing list: There is an associated Z FORUM mailing list. Articles are automatically cross-posted between comp.specification.z and the mailing list for those whose do not have access to USENET news. This may apply particularly to industrial Z users who are particularly encouraged to subscribe and post their experiences to the list. Contact with your name, address and e-mail address to join the mailing list. Messages for submission to the Z FORUM mailing list and the comp.specification.z newsgroup may be e-mailed to . Postal mailing list: If you wish to join the postal Z mailing list, please send your address to the industrial liaison secretary at the PRG in Oxford on . This will ensure you receive details of Z meetings, etc., particularly for people without access to electronic mail. 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 annual Z User Meetings held each December. 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 for further information on how to use the server. If anyone can provide FTP access to these files, please contact . 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 . Meetings: VDM'91 will be held on 21-25 October 1991, at Delft, the Netherlands. The meeting will include papers on Z. For further information, please e-mail the command "send z vdm91" to the PRG archive server. The 6th annual Z User Meeting will be held on 16-17 December 1991, at York University, England. Details will be distributed via comp.specification.z and Z FORUM. If you would like brief details of any other forthcoming Z-related meetings included here, please contact . This message was last updated on 3rd July 1991. -- Jonathan Bowen, Programming Research Group, Oxford University Computing Laboratory, UK. From ox-prg!s40883 Mon Jul 8 18:33:19 BST 1991 Article: 58 of comp.specification.z Path: ox-prg!s40883 From: s40883@zeus.usq.EDU.au (Mark A. Toleman) Newsgroups: comp.specification.z Subject: Please remove my name from the mailing list Message-ID: <9107081216.AA23205@zeus.usq.edu.au> Date: 8 Jul 91 12:16:27 GMT Sender: news@prg.ox.ac.uk Lines: 1 X-Mailer: mail-news 2.0.3 Status: O It's easier to read this in comp.specification.z From ox-prg!ukc!mcsun!uunet!munnari.oz.au!bunyip.cc.uq.oz.au!uqcspe!cs.uq.oz.au!brendan Mon Jul 8 18:33:56 BST 1991 Article: 59 of comp.specification.z Path: ox-prg!ukc!mcsun!uunet!munnari.oz.au!bunyip.cc.uq.oz.au!uqcspe!cs.uq.oz.au!brendan From: brendan@cs.uq.oz.au (Brendan Mahony) Newsgroups: comp.specification.z Subject: Re: The possible lack of popularity of Z in the industry Message-ID: <2347@uqcspe.cs.uq.oz.au> Date: 8 Jul 91 00:25:05 GMT References: <13946.9107051412@prg.oxford.ac.uk> <1991Jul5.165631.823@news.iastate.edu> Sender: news@cs.uq.oz.au Reply-To: brendan@cs.uq.oz.au Lines: 30 Status: O In <1991Jul5.165631.823@news.iastate.edu> taak9@isuvax.iastate.edu (Steve Sheldon) writes: >... it was the >general opinion of my project group that we would have been a >heck of a lot better off specifying our design in plain simple >english, possibly with FOPC to explain some points further. Perhaps you would like to give further detail of your experience so that some informed critical comment might be possible. What was the problem specified? Is the spec small enough for you to present it here? Perhaps with the English translation and why you feel it to be superior. >Our spec would have been easier to write, and certainly >easier to read, thus there were no advantages, just signifigant >disadvantages. One of the main points, of Z in any case, is that formal specs are EASIER to write and debug than English texts. They are usually at least one order of magnitude shorter. The suggest presentation style in Z is to write the spec in Z and then in English and to present both as a coherent specification document, with the Z parts being definitive and the English elaborative. -- Brendan Mahony | brendan@batserver.cs.uq.oz Department of Computer Science | heretic: someone who disgrees with you University of Queensland | about something neither of you knows Australia | anything about. From ox-prg!ian Mon Jul 8 18:34:40 BST 1991 Article: 60 of comp.specification.z Path: ox-prg!ian From: ian@minster.york.ac.uk Newsgroups: comp.specification.z Subject: Z tools Message-ID: Date: 8 Jul 91 10:55:53 GMT Sender: daemon@prg.ox.ac.uk Lines: 24 X-Mailer: mail-news 2.0.3 Status: O In article <26611.9107050600@prg.ox.ac.uk> in comp.specification.z, lrenshaw@uk.co.bt.axion (Laurence Renshaw) wrote... | ...what people really seem to want (IMO) is a real editor - | preferably WYSIWYG. I agree that many people want a WYSIWYG editor, but it isn't what most people need (though they often believe that it is!). There is another good reason for a tool not trying to be WYSIWYG: incremental tools (which is what good WYSIWYG tools have to be) are considerably harder to construct (said from personal experience, though not with Z). Even after considerably more testing/verification, I would have less trust in the correct operation of a WYSIWYG tool. And surely trustworthiness is particularly important for a Z tool. On a separate issue, there was some discussion entitled "The Best Z Tool". There are so many alternatives in the design of tools that they can be fairly compared only on the basis of particular user requirements (or preferences). What's best for one user may be useless to another. An independent evaluation of Z tools has been done by British Aerospace as part of the IED's ZIP project: their report may be of interest. If the discussion mentioned above has generated interest in CADiZ, you can write for further details to York Software Engineering Ltd, University of York, York, England YO1 5DD. From ox-prg!lrenshaw Mon Jul 8 18:35:23 BST 1991 Article: 61 of comp.specification.z Path: ox-prg!lrenshaw From: lrenshaw@axion.bt.co.uk (Laurence Renshaw) Newsgroups: comp.specification.z Subject: WYSIWYG tools (Re: Z tools) Message-ID: <5625.9107081219@orion.axion.bt.co.uk> Date: 8 Jul 91 12:19:33 GMT Sender: daemon@prg.ox.ac.uk Lines: 32 X-Mailer: mail-news 2.0.3 Status: O (reply to ian@minster.york.ac.uk's message): |I agree that many people want a WYSIWYG editor, but it isn't |what most people need (though they often believe that it is!). Why isn't it what they need ? How are they deluding themselves ? Are you saying that basic facilities are best and user-friendliness is fool's gold ? |There is another good reason for a tool not trying to be WYSIWYG: |incremental tools (which is what good WYSIWYG tools have to be) |are considerably harder to construct (said from personal experience, |though not with Z). Even after considerably more testing/verification, |I would have less trust in the correct operation of a WYSIWYG tool. |And surely trustworthiness is particularly important for a Z tool. What kind of trustworthiness are you referring to ? I never thought of a Z editor as a safety-critical application before, and I don't think reliable WYSIWYG editors are that uncommon or difficult to build. We have a WYSIWYG Z editor here which works quite well (it's not in the ZIP report). Although the printed output of some WYSIWYG tools may not look _exactly_ the same as the screen picture (e.g. the spacing may be slightly changed), it's still better than trying to guess what latex or troff will do. |If the discussion mentioned above has generated interest in CADiZ, |you can write for further details to York Software Engineering Ltd, |University of York, York, England YO1 5DD. Maybe zforum should sell advertising space :-) From ox-prg!ukc!warwick!covpoly!cck.cov.ac.uk!unreplyable!garbage Tue Jul 9 11:22:09 BST 1991 Article: 62 of comp.specification.z Path: ox-prg!ukc!warwick!covpoly!cck.cov.ac.uk!unreplyable!garbage From: csx040@cck.cov.ac.uk (Alan Chantler (CS)) Newsgroups: comp.specification.z Subject: Re: (none) Message-ID: Date: 8 Jul 91 09:42:18 GMT References: Organization: Coventry Polytechnic, Coventry, UK Lines: 16 Status: O In article wang@minster.york.ac.uk writes: >| 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: > >I'd be interested in a copy of the Object-z reference manual too. Because I don't know the e-mail address of Queensland please may I request a copy of this document via 'news' ? -- AlanC@coventry.ac.uk | Post: Coventry Polytechnic JANET: AlanC@uk.ac.coventry | Priory Street INET : AlanC%coventry.ac.uk@nsfnet-relay.ac.uk | Coventry, UK Phone: +44 203 838332 | CV1 5FB From ox-prg!nick Tue Jul 9 11:38:20 BST 1991 Article: 63 of comp.specification.z Path: ox-prg!nick From: nick@logcam.co.uk (nick) Newsgroups: comp.specification.z Subject: Please remove my name from the mailing list Message-ID: <1137.9107081641@tigger.logcam.co.uk> Date: 8 Jul 91 16:41:03 GMT Sender: daemon@prg.ox.ac.uk Lines: 1 X-Mailer: mail-news 2.0.3 Status: O From ox-prg!ian Tue Jul 9 11:40:56 BST 1991 Article: 64 of comp.specification.z Path: ox-prg!ian From: ian@minster.york.ac.uk Newsgroups: comp.specification.z Subject: Re: Z tools Message-ID: Date: 8 Jul 91 21:20:27 GMT Sender: daemon@prg.ox.ac.uk Lines: 81 X-Mailer: mail-news 2.0.3 Status: O Lawrence Renshaw asks me about WYSIWYG editors... The functionality provided by a WYSIWYG editor basically corresponds to pointing at things and doing operations on them. The idiom doesn't cope well with relations between several things. Some operations that are difficult for a WYSIWYG Z editor include typesetting every use of an operator in exactly the same fancy way, e.g. as a subscript, and preparing a typeset index of where each symbol is used in a document. And don't forget the informal parts of a Z specification: all that explanatory text with diagrams, tables, etc should be editable too. So the claim that a non-WYSIWYG tool can provide only "basic facilities" is false: it can provide facilities that a WYSIWYG tool would find hard. This is not to say that a WYSIWYG tool is not user-friendly, only that it cannot provide these facilities in a more user-friendly way. My ideal Z tool might well be a WYSIWYG one. What I said before was that I don't need one. Let me explain some more of the issues concerning my ideal WYSIWYG Z editor - maybe that'll help you to understand my viewpoint. (This could get long - apologies in advance.) Editing should be text-oriented, not structured or syntax-directed. Although useful for novices, syntax-directed editing quickly becomes a pain. The text-oriented approach is quicker and easier in the long run. Inserting or deleting text may change the page layout of the rest of the specification document, requiring it to be re-typeset. Declarations may move to different pages, requiring any index to be re-typeset too. Since the user is interacting with the tool in real time, response times are important. The user may be prepared to wait for the current page to be re-typeset, but will want to resume the interaction immediately thereafter. At intervals (perhaps when a change is committed), the tool should check that the entire specification conforms to the syntax, scope and type rules of the Z language. At least for large specifications, this checking must be done incrementally to ensure satisfactory response times. The idea of incremental checking is to avoid re-checking those parts that couldn't possibly be affected by the change. As an example, consider removal of a declaration from a named schema. All references that were bound to that declaration should be indicated as erroneous. Such references might be found in the predicate part of the same schema, in schemas that include the modified one, possibly indirectly through several inclusions, and in certain kinds of schema calculus expressions. (An incremental checker might remember exactly where these references are to further optimize this suggested search.) If the removed declaration is that of an operator having special lexical status (e.g. infix), there is a further problem: syntax errors might be introduced in previously correct schemas which used that operator. I'm not at all sure that these are all the possible consequences of removing a declaration of this particular kind, and there are many more kinds of change to consider. Note that the integration needed between editor and checker is so tight that they cannot easily be separated. The user-interface should maintain an exploratory style, i.e. not put unnecessary constraints on the user's work. For example, it shouldn't be necessary to fix an error in the specification the moment it is detected. Rather, the user should be able to complete present intentions, and come back afterwards to resolve any errors that might still remain. Note that there is no need to report the specific errors to the user in the meantime, only to notify that there are some errors and be ready to show them should the user wish to inspect them. In conclusion, my colleagues would still be waiting for my WYSIWYG Z editor if I'd decided to build it. They've tried a couple of WYSIWYG Z tools, but haven't yet found one that they'd choose to use. Perhaps my concerns about trustworthiness are more understandable now. When checking is done incrementally, it is easy to overlook checking for a particular consequence of a particular change. The main field in which a Z editor might actually be used (ignoring universities and polytechnics) is in the development of safety critical systems, where its reliability is surely important. | Maybe zforum should sell advertising space :-) There's an easy criticism if ever there was one! I gave the address of YSE Ltd in the hope that it would reduce discussion of a commercial product in this forum - I knew I couldn't win! Note that the rest of that article, and the entirety of this one, contains no mention of CADiZ. (Oops, I said it after all :-) From ox-prg!ukc!mcsun!uunet!zaphod.mps.ohio-state.edu!hobbes.physics.uiowa.edu!news.iastate.edu!vaxf.iastate.edu!TAAK9 Tue Jul 9 11:41:55 BST 1991 Article: 65 of comp.specification.z Path: ox-prg!ukc!mcsun!uunet!zaphod.mps.ohio-state.edu!hobbes.physics.uiowa.edu!news.iastate.edu!vaxf.iastate.edu!TAAK9 From: taak9@isuvax.iastate.edu (Steve Sheldon) Newsgroups: comp.specification.z Subject: Re: The possible lack of popularity of Z in the industry Message-ID: <1991Jul8.150538.5723@news.iastate.edu> Date: 8 Jul 91 15:05:38 GMT References: <13946.9107051412@prg.oxford.ac.uk> <1991Jul5.165631.823@news.iastate.edu>,<2347@uqcspe.cs.uq.oz.au> Sender: news@news.iastate.edu (USENET News System) Reply-To: taak9@isuvax.iastate.edu Organization: Iowa State University, Ames, IA. Lines: 54 Status: O In article <2347@uqcspe.cs.uq.oz.au>, brendan@cs.uq.oz.au (Brendan Mahony) writes: > >In <1991Jul5.165631.823@news.iastate.edu> taak9@isuvax.iastate.edu (Steve Sheldon) writes: > >>... it was the >>general opinion of my project group that we would have been a >>heck of a lot better off specifying our design in plain simple >>english, possibly with FOPC to explain some points further. > >Perhaps you would like to give further detail of your experience so that >some informed critical comment might be possible. What was the problem >specified? Is the spec small enough for you to present it here? Perhaps >with the English translation and why you feel it to be superior. > >>Our spec would have been easier to write, and certainly >>easier to read, thus there were no advantages, just signifigant >>disadvantages. > >One of the main points, of Z in any case, is that formal specs are >EASIER to write and debug than English texts. They are usually >at least one order of magnitude shorter. > >The suggest presentation style in Z is to >write the spec in Z and then in English and to present both as a >coherent specification document, with the Z parts being definitive and >the English elaborative. > Well, we were told to describe a B*-Tree and related operations. Didn't seem to useful at the time. There was no "reason" to use a B*-Tree, it was just there. We didn't use Z, or anything remotely popular. The language was something dreamed up by a faculty member, and described in a handful of photocopied sheets. So we didn't have very many examples, and so we did not receive much experience at reading others specs. I guess I just found my experience with the class somewhat frustrating. It was unfortunate, I was able to read a couple of books on software engineering that I found in our library, and they were quite different, even describing things that would actually be helpful to use. I find it interesting, that Z suggests presenting specifications with english descriptions as well. It seemed to me in writing our spec, that it required a great deal of comments. Or at least it would have been easier to understand what the author intended to say. Steve Sheldon taak9@ccvax.iastate.edu Computer Science undergrad Iowa State University From ox-prg!ukc!icdoc!sot-ecs!amg Tue Jul 9 11:43:28 BST 1991 Article: 66 of comp.specification.z Path: ox-prg!ukc!icdoc!sot-ecs!amg From: amg@ecs.soton.ac.uk (Andy Gravell) Newsgroups: comp.specification.z Subject: Re: The possible lack of popularity of Z in the industry Message-ID: <8437@ecs.soton.ac.uk> Date: 8 Jul 91 10:44:20 GMT References: <13946.9107051412@prg.oxford.ac.uk> <1991Jul5.165631.823@news.iastate.edu> Sender: news@ecs.soton.ac.uk Lines: 58 Status: O In <1991Jul5.165631.823@news.iastate.edu> taak9@isuvax.iastate.edu (Steve Sheldon) writes: > I recently had the overwhelming joy of taking a class in Software >Engineering, where we were supposedly going to learn all about >specifications and the design process. I don't recall learning >anything of any particular use, just a bunch of academic theory. > Well, after this experience, I have to agree with the last >two arguments above why few individuals use these tools. The teaching >materials used in our class explained nothing. And it was the >general opinion of my project group that we would have been a >heck of a lot better off specifying our design in plain simple >english, possibly with FOPC to explain some points further. >Our spec would have been easier to write, and certainly >easier to read, thus there were no advantages, just signifigant >disadvantages. Well, I cannot let this go by. What's so good about a spec being easy to write and/or easy to read? "The system must be user-friendly." There - that's easy to write, and I've certainly read it many times (often describing systems that *I* thought were most unfriendly). The problem with your plain simple english is that, all too often it is loose, ambiguous and subject to different interpretations. For example, I reach for my DOS manual, and glance at the BACKUP command where I am told about various switches such as /b[:date] Backs up only those files dated on or before the specified date (entered in any of the forms mm-dd-yy dd-mm-yy or yy-mm-dd). /g or /s Globally backs up files in all subdirectories as well as the files in the current working directory. /m or /w Backs up only *written files* - those that have been changed since the last backup was made. (Extracts from Microsoft MS-DOS Version 3.21 User's Guide and Reference, as supplied by Zenith Data Systems). As a user of the software, I am left in doubt by the manual. I can think of at least two contradictory interpretations of each sentence. I expect you can too. For example does /g back up all subdirectories of the current drive, or just the current directory? Of course, I could run a little test to find out easily enough - but a) life is too short, and b) I would only do that if I was suspicious enough to spot the ambiguities. Now, this is not so much an argument in favour of formal specification, as an argument *against* using English alone. An entertaining paper by Bertrand Meyer argues that using formal notation is in fact a good way to improve your English description as well. (On Formalism in Specifications, IEEE Software, Vol 2, No 1, pages 6-20.) It is well worth reading. I am sorry that your course was effective only in turning you off formal notation. Andy Gravell From ox-prg!ukc!mcsun!uunet!cis.ohio-state.edu!zaphod.mps.ohio-state.edu!ncar!csn!cherokee!tonto!zhu Tue Jul 9 11:44:13 BST 1991 Article: 67 of comp.specification.z Path: ox-prg!ukc!mcsun!uunet!cis.ohio-state.edu!zaphod.mps.ohio-state.edu!ncar!csn!cherokee!tonto!zhu From: zhu@tonto (Jianhua Zhu) Newsgroups: comp.specification.z Subject: Re: FDTs and Graphical Notations (was Re: Prove me wrong) Message-ID: <1991Jul8.184523.4807@cherokee.uswest.com> Date: 8 Jul 91 18:45:23 GMT References: <1991Jul2.105231.20473@fmg.bt.co.uk> <1991Jul5.145042.8664@porthos.cc.bellcore.com> Sender: news@cherokee.uswest.com (Telegraph Row) Organization: U S WEST Advanced Technologies Lines: 68 Nntp-Posting-Host: tonto.uswest.com Status: O In article <1991Jul5.145042.8664@porthos.cc.bellcore.com> haim@taichi.UUCP (24122-Haim Kilov) writes: >91Jul5093551@scarlett.otca.oz.au> >Sender: netnews@porthos.cc.bellcore.com (USENET System Software) >Reply-To: haim@taichi.UUCP (24122-Haim Kilov) >Organization: Bellcore, Livingston, NJ >Lines: 58 > >In article karenr@otca.oz.au (Karen Rosenberg) writes: >... >>Formal techniques have the advantage that they can completely model a >>system in a rigorous, correct manner. However, many customers out there do >>not come from a mathematical or computing background, so will find it >>difficult to understand such specifications. The use of a diagramming >>technique along the lines of DFDs or ERDs can act as an "interface" to the >>more complete formal specification. In a sense, the diagrams would guide >>the reader through the formal specification. >> >>It may be difficult, however, to integrate a particular diagramming >>technique and formal description technique. A related possibility is that >>a formal description technique may be able to act as a "backbone" reference >>for the variety of techniques used and diagrams produced during the >>different phases of software development. For example, a particular class >>in Object-Z will contain a state and operations on that state. The state >>part will correspond to an ERD whereas the operations "may" correspond to a >>DRD. It remains to be seen how well this would work. >> >I agree with the "guidance" idea. However, the guides may be incomplete >and sometimes even misleading (to quote Bertrand Meyer, "try to find seven >errors in a picture"). They should be used with care. > >On the last paragraph, it is not so easy to agree. ERD represent MORE than >just "state part": by means of defining a thing as a relationship, or a weak >entity, or a composite entity, or ..., important behavioral (CRUD) >properties of this thing and associated things are defined. Therefore at >least some generic operations for the thing are defined. > ... >haim@bcr.cc.bellcore.com I would not say that ERDs represent more than system states, although I'd qualify "system states" with the word "valid". Namely, ERDs can represent valid system states, through the use of a set of rich semantic constructs, including composite entities/weak entities as already mentioned, and contraining mechanisms such as cardinality constraints, referential integrity, etc. The important behavioral aspect of an ERD as you put it, namely CRUD, is interesting in that it is an attempt at modeling certain system dynamics statically. In particular, I consider the CRUD relationship a more detailed version of the notion of signature for operations (as it allows expressing the actual effect (Create, Read, Update and Delete) on the types involved in an operation. Consequently, it is possible to build a more powerful type checker to uncover design errors. Nevertheless, CRUD is still a static representation of the properties for operations. One thing I have a hard time to understand, though, is that there seems to be a general concensus in this thread of discussion that ERDs are informal when compared with other notations such as Z. I don't se