From nic.csu.net!usc!cs.utexas.edu!uunet!pipex!uknet!comlab.ox.ac.uk!vnet.IBM.COM Fri Jun 4 17:05:58 1993 Relay-Version: VMS News - V6.1B5 17/9/92 VAX/VMS V5.5-2; site nic.csu.net Path: nic.csu.net!usc!cs.utexas.edu!uunet!pipex!uknet!comlab.ox.ac.uk!vnet.IBM.COM Newsgroups: comp.specification.z Subject: Executable Specifications May Be Hazardous to Your Product Message-ID: <19930526.115422.RYMAN@TOROLAB2> From: ryman@vnet.IBM.COM (Arthur Ryman) Date: 26 May 93 11:54:22 EDT X-Mailer: mail-news 2.0.3 Lines: 35 Status: O From: Arthur Ryman Phone: (416) 448-3077, TIE 778-3077, FAX (416) 448-4414 There has been a lot of talk recently about generating executable code (Prolog, C) from Z. At first sight this seems attractive. It would certainly be handy to test a specification against one's expectations. However, there is a danger here. Unlike most other languages (whose purpose is to communicate a human's intentions to a computer), Z's main purpose is to communicate one human's intentions to another human. Z is a vehicle for a group of humans to come to a consensus about what should be built. The overriding concern here is for clarity. If people begin to use Z to tell a computer what to do, then the goal of clarity may start to give way to concerns of efficiency, and I feel that would be a big mistake. If you're at the point of knowing exactly what you want to build, then perhaps it's time to cut over to a high level prototyping language, functional or otherwise. There is a place in the development cycle for a language like Z that completely ignores the issue of executability. This means the spec can be incomplete and use highly inefficient data models. This freedom should be used by the specifier to achieve clarity. Let's not push the incidental complexity associated with implementation up to the front of the cycle where we are trying to cope with the essential complexity of the application. . Sincerely yours, Dr. A.G.(Arthur) Ryman, Senior Development Analyst, AD Tools IBM Canada Laboratory, 3G/611/1150/TOR 1150 Eglinton Avenue East, North York, Ontario, M3C 1H7 Canada From nic.csu.net!usc!cs.utexas.edu!uwm.edu!caen!batcomputer!ghost.dsi.unimi.it!univ-lyon1.fr!scsing.switch.ch!josef!ifimac63.ifi.unizh.ch!user Fri Jun 4 17:06:51 1993 Relay-Version: VMS News - V6.1B5 17/9/92 VAX/VMS V5.5-2; site nic.csu.net Path: nic.csu.net!usc!cs.utexas.edu!uwm.edu!caen!batcomputer!ghost.dsi.unimi.it!univ-lyon1.fr!scsing.switch.ch!josef!ifimac63.ifi.unizh.ch!user Newsgroups: comp.specification.z Subject: Re: Executable Specifications May Be Hazardous to Your Product Message-ID: From: fuchs@ifi.unizh.ch (Norbert E. Fuchs) Date: Thu, 3 Jun 1993 15:35:58 GMT Sender: news@ifi.unizh.ch (USENET News Admin) Followup-To: comp.specification.z References: <19930526.115422.RYMAN@TOROLAB2> Organization: IFI University of Zurich Nntp-Posting-Host: ifimac63 Lines: 61 Status: O In article <19930526.115422.RYMAN@TOROLAB2>, ryman@vnet.IBM.COM (Arthur Ryman) wrote: > > There has been a lot of talk recently about generating executable code > (Prolog, C) from Z. At first sight this seems attractive. It would > certainly be handy to test a specification against one's expectations. > However, there is a danger here. > > Unlike most other languages (whose purpose is to communicate a human's > intentions to a computer), Z's main purpose is to communicate one human's > intentions to another human. Z is a vehicle for a group of humans to come > to a consensus about what should be built. The overriding concern here is > for clarity. > So are executable specifications which serve to clarify and complete requirements/specifications, and to be the basis for a consensus between the possible heterogeneous group of people involved (application specialists, users, software developers). > > If people begin to use Z to tell a computer what to do, then the goal > of clarity may start to give way to concerns of efficiency, and I feel > that would be a big mistake. > I addressed this topic in my paper "Specifications Are (Preferably) Executable" (Software Engineering Journal, vol. 7, no. 5, September 1992, pp. 323-333) in which I show that clarity and executability are not mutually exclusive. > > If you're at the point of knowing exactly what you want to build, then > perhaps it's time to cut over to a high level prototyping language, > functional or otherwise. > To serve as an explorative prototype is exactly one of the motivations to make specifications executable. Many requirements - especially nonfunctional ones like user interactions - can only be decided on the basis of experience. There are situations when reasoning and arguing alone does not provide a sufficient basis for decisions. > > There is a place in the development cycle for a language like Z that > completely ignores the issue of executability. This means the spec > can be incomplete and use highly inefficient data models. This freedom > should be used by the specifier to achieve clarity. > At least in our system, specifications can be incomplete and executable, and - if you wish (;-) - also inefficient. > > Let's not push the > incidental complexity associated with implementation up to the front of > the cycle where we are trying to cope with the essential complexity of > the application. > Again, executability does not necessarily mean complexity. ------------------------------------------------------------------------------ Norbert E. Fuchs Telephone +41-1-257 4313 Institute for Informatics Fax +41-1-363 0035 University of Zurich email fuchs@ifi.unizh.ch CH-8057 Zurich, Switzerland ------------------------------------------------------------------------------ From nic.csu.net!usc!howland.reston.ans.net!agate!doc.ic.ac.uk!uknet!comlab.ox.ac.uk!comlab.ox.ac.uk!joy Thu Sep 23 10:09:55 1993 Relay-Version: ANU News - V6.1 08/24/93 VAX/VMS V5.5-2; site nic.csu.net Path: nic.csu.net!usc!howland.reston.ans.net!agate!doc.ic.ac.uk!uknet!comlab.ox.ac.uk!comlab.ox.ac.uk!joy Newsgroups: comp.specification.z Subject: Z Short Course Message-ID: <1993Sep20.144413.1052@peppone.comlab.ox.ac.uk> From: joy@comlab.ox.ac.uk (Joy Reed) Date: Mon, 20 Sep 1993 14:44:13 GMT Sender: joy@comlab.ox.ac.uk (Joy Reed) Organization: Oxford University Computing Laboratory, UK Originator: joy@peppone.comlab Lines: 109 Status: O Formal Systems (Europe), Ltd Preliminary Course Announcements: ------------------------------ Formal Development Using Z and Advanced Z ------------------------------ Nov 29 - Dec 3, 1993 Boston, MA Course Lecturer: J.C.P. Woodcock Formal Systems (Europe) Ltd exploits pioneering work in the field of Formal Methods. The directors and staff include key current and former members of the Programming Research Group at Oxford University, England, each with an established international reputation. The company has extensive industrial experience of the pragmatic application of formal techniques to the analysis and design of both software and hardware systems, in Europe and the USA. Since its formation in 1989, Formal Systems has expanded rapididly, both in staff and revenue. Past and present clients for consultancy include Inmos Ltd on VLSI design quality assurance, Deutsche System Technik on formal specification, C.S. Draper Laboratory on fault-tolerant processors, and Secure Information Systems Ltd on formal verification. Additionally, Formal Systems is a collaborator in European Community ESPRIT activities and has given specialized industrial short courses in conjunction with Oxford University in the UK and Tulane University in the USA. In 1991 Formal Systems received a prestigious SMART Award from the UK Department of Trade and Industry for technological innovation in an aerospace engineering application. Z is a specification language based on mathematical set theory and logic. It was developed at Oxford University for use in the specification of state-based programs, and has now matured into a valuable and widely used development tool. For example, IBM UK Laboratories at Hursley have used Z to develop approximately 48,000 lines of new code for the CICS system (the main IBM System/370 on-line transaction processing system). They obtained a significant reduction in the volume of software quality defects for ultimately little additional development cost. For this achievement, IBM UK Laboratories and Oxford University Computing Laboratory (PRG) were jointly presented with a prestigious Queen's Award for Technological Achievement in 1992. Z has proved itself to be especially useful as a tool for formally verifying and demonstrating the correctness of safety critical and/or secure systems. Formal Development Using Z: --------------------------- We present the Z notation, together with systematic techniques for developing designs and code from Z specifications. Mechanical assistance in managing specification and proof will be demonstrated using an automated proof assistant. An understanding of elementary logic and set theory is useful. Advanced Z: ----------- This course is intended for those already familiar with the Z notation. We describe how specifications in Z can be accurately implemented as programs. We discuss both data refinement and operation development, and present the ideas through case studies. Dr J. C. P. Woodcock is Director of External Studies at Oxford University Computing Laboratory, as well as being a Director of Formal Systems. His research interests include specification, refinement and proof of sequential and concurrent systems, security, and technology transfer. He has been a consultant for IBM for the last six years working on formally specifying and analyzing the CICS system. As a consultant to IBM for six years, he was a key member of the team that won the Queen's Award (see above) for specifying and analyzing the CICS system. He has taught courses in formal methods to over 1500 students from industry and academia. Location Boston (area) MA USA Date Nov 29 - Dec 3, 1993 Duration Four and a half days (ends lunchtime Friday) Course Fee $xxxx per person includes course materials, lunches and a course dinner. Inquire for block rates. (News posting rules prohibit price information for commercial ventures. Please contact us for details.) Accommodation Hotel accommodation is available for ~$xx/night plus tax. Contact Dr Joy Reed Ms Kate Pearson Joy.Reed@prg.ox.ac.uk (Address below) Formal Systems (Europe) Ltd, 3 Alfred Street, Oxford OX1 4EH UK, Tel: +44 865 728460, FAX: +44 865 201114 (There is at least +5 hours time difference between the UK and US.) From rbotting@wiley.csusb.edu Fri Jan 28 14:57 PST 1994 Return-Path: Received: from wiley.csusb.edu by silicon.csci.csusb.edu (5.0/SMI-SVR4) id AA28586; Fri, 28 Jan 94 14:57:09 PST Received: by wiley.csusb.edu (5.67a/1.34) id AA03298; Fri, 28 Jan 1994 14:58:34 -0800 Date: Fri, 28 Jan 1994 14:58:34 -0800 From: rbotting@wiley.csusb.edu ("Dr. Richard Botting") Message-Id: <199401282258.AA03298@wiley.csusb.edu> To: dick@silicon.csci.csusb.edu Subject: (fwd) Re: fuzz Newsgroups: comp.specification.z Content-Type: text Content-Length: 1322 Status: RO Path: csus.edu!decwrl!nic.hookup.net!news.moneng.mei.com!howland.reston.ans.net!ee.und.ac.za!hippo.ru.ac.za!itu1.sun.ac.za!hloedolf From: hloedolf@cs.sun.ac.za (H L Loedolff) Newsgroups: comp.specification.z Subject: Re: fuzz Date: 20 Jan 1994 10:29:48 GMT Organization: Stellenbosch University, South Africa Lines: 23 Message-ID: <2hlmes$5q4@itu1.sun.ac.za> References: Reply-To: hloedolf@cs.sun.ac.za NNTP-Posting-Host: itu1.sun.ac.za X-Newsreader: TIN [version 1.2 PL1] david@mvision.com wrote: > Hi, > Can anyone tell me how to get the "fuzz" package, or for that > matter, any automated Z tool ? Fuzz is a comercial package. E-mail mike@uk.ac.oxford.prg for more information. There is a free z stylesheet for \LaTex that comes with fuzz. It may be ftp'ed from ftp.comlab.ox.ac.uk. There is only one free type checker, named ZTC. Unfortunately it only runs on DOS and is still a bit unstable, but it is a very promising program. ZTC may be obtained at ise.cs.depaul.edu in directory /dist as ZTC1.2.tar.Z Good luck! -- -Hans hloedolf@itu.sun.ac.za -- rbotting@wiley.csusb.edu. rbotting::=`Dr. Richard J. Botting`, wiley::=`Faculty EMail System`, csusb::=`California State University, San Bernardino, CA 92407, USA`. From rbotting@wiley.csusb.edu Wed Feb 2 18:51 PST 1994 Return-Path: Received: from wiley.csusb.edu by silicon.csci.csusb.edu (5.0/SMI-SVR4) id AA17498; Wed, 2 Feb 94 18:51:45 PST Received: by wiley.csusb.edu (5.67a/1.34) id AA08758; Wed, 2 Feb 1994 18:53:06 -0800 Date: Wed, 2 Feb 1994 18:53:06 -0800 From: rbotting@wiley.csusb.edu ("Dr. Richard Botting") Message-Id: <199402030253.AA08758@wiley.csusb.edu> To: dick@silicon.csci.csusb.edu Subject: (fwd) How good is Fuzz? Newsgroups: comp.specification.z Content-Type: text Content-Length: 1215 Status: RO Newsgroups: comp.specification.z Path: csus.edu!netcom.com!netcomsv!decwrl!decwrl!nic.hookup.net!usc!howland.reston.ans.net!pipex!slxsys!bae-st!usenet From: stephen@def.bae.co.uk (Stephen Paynter) Subject: How good is Fuzz? Message-ID: <1994Jan25.102706.14386@def.bae.co.uk> Sender: usenet@def.bae.co.uk Reply-To: stephen@def.bae.co.uk Organization: British Aerospace (Dynamics) Ltd Date: Tue, 25 Jan 94 10:27:06 GMT Lines: 16 I am in the process of writing an internal Evaluation report for my company on Fuzz. A section of such a report has to report on the general consensus about the tool being evaluated. Therefore: Are there any known problems with version 2.1 of Fuzz? How is it generally perceived by users? Thank you to anyone who can spare the time to reply, Stephen ================================================================================ Dr. S.E. Paynter, Senior Software Engineer, BAe Defence Ltd., Dynamics Division, FPC 450, P.O. Box 5, Filton, Bristol, BS12 7QW. Telephone: (UK) 0272 316108 -- rbotting@wiley.csusb.edu. rbotting::=`Dr. Richard J. Botting`, wiley::=`Faculty EMail System`, csusb::=`California State University, San Bernardino, CA 92407, USA`. From rbotting@wiley.csusb.edu Wed Feb 2 18:51 PST 1994 Return-Path: Received: from wiley.csusb.edu by silicon.csci.csusb.edu (5.0/SMI-SVR4) id AA17499; Wed, 2 Feb 94 18:51:46 PST Received: by wiley.csusb.edu (5.67a/1.34) id AA08762; Wed, 2 Feb 1994 18:53:07 -0800 Date: Wed, 2 Feb 1994 18:53:07 -0800 From: rbotting@wiley.csusb.edu ("Dr. Richard Botting") Message-Id: <199402030253.AA08762@wiley.csusb.edu> To: dick@silicon.csci.csusb.edu Subject: (fwd) How good is Fuzz? Newsgroups: comp.specification.z Content-Type: text Content-Length: 3069 Status: RO Newsgroups: comp.specification.z Path: csus.edu!csulb.edu!library.ucla.edu!europa.eng.gtefsd.com!howland.reston.ans.net!pipex!uknet!comlab.ox.ac.uk!vnet.IBM.COM From: ryman@vnet.IBM.COM (Arthur Ryman) Subject: How good is Fuzz? Message-ID: <19940128.151358.RYMAN@TOROLAB2> Date: 28 Jan 94 15:13:57 EST X-Mailer: mail-news 2.0.3 Comments: Forwarding note of Thu, 27 Jan 94 20:25:57 GMT from Lines: 60 From: Arthur Ryman Phone: (416) 448-3077, TIE 778-3077, FAX (416) 448-4414 I have used fuzz on RS/6000 and Macintosh/MPW. Both versions seem solid. I was especially impressed by the speed of fuzz on RS/6000. The Macintosh worked well with OzTeX. I tested fuzz on the sample documents provided with it and it performed as advertised. I also used fuzz on an article and specs I wrote and I found the error messages clear and helpful. Sincerely yours, Dr. A.G.(Arthur) Ryman, Senior Development Analyst, AD Tools IBM Canada Laboratory, 3G/611/1150/TOR 1150 Eglinton Avenue East, North York, Ontario, M3C 1H7 Canada *** Forwarding note from SMTP2 --IINUS1 01/27/94 15:45 *** ========================================================================= Received: from sun2.nsfnet-relay.ac.uk by vnet.IBM.COM (IBM VM SMTP V2R2) with TCP; Thu, 27 Jan 94 15:45:07 EST Via: uk.ac.oxford.comlab; Thu, 27 Jan 1994 20:32:16 +0000 Received: by comlab.ox.ac.uk id AA16370; Thu, 27 Jan 94 20:26:05 GMT Sender: zforum-request@comlab.oxford.ac.uk Precedence: bulk Received: from comlab.oxford.ac.uk (mail.comlab) by comlab.ox.ac.uk id AA16362; Thu, 27 Jan 94 20:26:00 GMT Received: from comlab.ox.ac.uk (inca.comlab) by comlab.oxford.ac.uk id AA08407; Thu, 27 Jan 94 20:25:27 GMT Received: by comlab.ox.ac.uk id AA16356; Thu, 27 Jan 94 20:25:57 GMT Message-Id: <16356.9401272025@comlab.ox.ac.uk> Date: Thu, 27 Jan 94 20:25:57 GMT Path: comlab.ox.ac.uk!uknet!pipex!slxsys!bae-st!usenet From: stephen@defence.british-aerospace.co.uk (Stephen Paynter) To: zforum@comlab.oxford.ac.uk Subject: How good is Fuzz? Original-Message-Id: <1994Jan25.102706.14386@def.bae.co.uk> Original-Date: Tue, 25 Jan 94 10:27:06 GMT Original-Sender: usenet@defence.british-aerospace.co.uk Reply-To: stephen@defence.british-aerospace.co.uk Organization: British Aerospace (Dynamics) Ltd Lines: 16 I am in the process of writing an internal Evaluation report for my company on Fuzz. A section of such a report has to report on the general consensus about the tool being evaluated. Therefore: Are there any known problems with version 2.1 of Fuzz? How is it generally perceived by users? Thank you to anyone who can spare the time to reply, Stephen ============================================================================== == Dr. S.E. Paynter, Senior Software Engineer, BAe Defence Ltd., Dynamics Division, FPC 450, P.O. Box 5, Filton, Bristol, BS12 7QW. Telephone: (UK) 0272 316108 -- rbotting@wiley.csusb.edu. rbotting::=`Dr. Richard J. Botting`, wiley::=`Faculty EMail System`, csusb::=`California State University, San Bernardino, CA 92407, USA`. From rbotting@wiley.csusb.edu Wed Feb 2 18:51 PST 1994 Return-Path: Received: from wiley.csusb.edu by silicon.csci.csusb.edu (5.0/SMI-SVR4) id AA17503; Wed, 2 Feb 94 18:51:47 PST Received: by wiley.csusb.edu (5.67a/1.34) id AA08766; Wed, 2 Feb 1994 18:53:08 -0800 Date: Wed, 2 Feb 1994 18:53:08 -0800 From: rbotting@wiley.csusb.edu ("Dr. Richard Botting") Message-Id: <199402030253.AA08766@wiley.csusb.edu> To: dick@silicon.csci.csusb.edu Subject: (fwd) Re: How good is Fuzz? Newsgroups: comp.specification.z Content-Type: text Content-Length: 2950 Status: RO Path: csus.edu!netcom.com!netcomsv!decwrl!elroy.jpl.nasa.gov!swrinde!cs.utexas.edu!howland.reston.ans.net!EU.net!Germany.EU.net!Informatik.Uni-Dortmund.DE!paris!willi From: willi@paris.informatik.uni-dortmund.de (Wilhelm Hasselbring ) Newsgroups: comp.specification.z Subject: Re: How good is Fuzz? Date: 31 Jan 1994 09:13:07 GMT Organization: CS Department, University of Dortmund, Germany Lines: 39 Message-ID: <2iii33$cq8@fbi-news.informatik.uni-dortmund.de> References: <1994Jan25.102706.14386@def.bae.co.uk> NNTP-Posting-Host: paris.informatik.uni-dortmund.de X-Newsreader: TIN [version 1.2 PL2] Stephen Paynter (stephen@def.bae.co.uk) wrote: : I am in the process of writing an internal Evaluation report for my company : on Fuzz. A section of such a report has to report on the general consensus about : the tool being evaluated. Therefore: : Are there any known problems with version 2.1 of Fuzz? : : How is it generally perceived by users? I used fuzz on Sun Workstations. It is a stable program. However, while constructing specifications with fuzz I recognized an important drawback of using Z with the fuzz package: the principle of definition before use, which leads to a bottom-up development of the specification. It would be more natural to write and explain the specification in a top-down manner. The important point with Z is just that any specification must be written in a way such that its definitions can be ordered to satisfy the principle of definition before use (see Mike Spivey's ZRM, 2nd ed, page 47). This avoids recursive definitions in which a schema includes itself. Therefore, it should be possible to develop a tool for Z that allows the introduction of paragraphs in any order and ensures that the principle of definition before use can be satisfied. I propose a fuzz directive, which *announces* a forthcoming definition before its use. This announcement should be invisble and it should only include the declaration part, not the predicates. fuzz could check the correspondence with the final definition. The existing fuzz directives allow preliminary, invisible definitions, but the later final definitions cannot be type-checked because they are redefinitions of global names. One could copy the formulae of the final definition into the preliminary, invisible definition, but then it would become impractical to change the specification. Regards, Willi --------------------- Willi Hasselbring Email: willi@ls10.informatik.uni-dortmund.de University of Dortmund Tel.: ++49 +231 755.4712 //// FB 4, LS Informatik 10 Fax: ++49 +231 755.2061 UNI DO Campus Sued Software Technology Baroper Str. 301 \*\ //// Building IV D-44221 Dortmund, Germany \\\/// Room 309 -- rbotting@wiley.csusb.edu. rbotting::=`Dr. Richard J. Botting`, wiley::=`Faculty EMail System`, csusb::=`California State University, San Bernardino, CA 92407, USA`. From rbotting@wiley.csusb.edu Wed Feb 2 18:51 PST 1994 Return-Path: Received: from wiley.csusb.edu by silicon.csci.csusb.edu (5.0/SMI-SVR4) id AA17504; Wed, 2 Feb 94 18:51:48 PST Received: by wiley.csusb.edu (5.67a/1.34) id AA08770; Wed, 2 Feb 1994 18:53:09 -0800 Date: Wed, 2 Feb 1994 18:53:09 -0800 From: rbotting@wiley.csusb.edu ("Dr. Richard Botting") Message-Id: <199402030253.AA08770@wiley.csusb.edu> To: dick@silicon.csci.csusb.edu Subject: (fwd) Re: How good is Fuzz? Newsgroups: comp.specification.z Content-Type: text Content-Length: 3222 Status: RO Newsgroups: comp.specification.z Path: csus.edu!wupost!mont!golf!zombie.ncsc.mil!paladin.american.edu!howland.reston.ans.net!pipex!uknet!comlab.ox.ac.uk!src.bae.co.uk From: Michael.Benjamin@src.bae.co.uk (Michael Benjamin) Subject: Re: How good is Fuzz? Message-ID: <9401311402.AA00491@sun53.src.bae.co.uk> Date: Mon, 31 Jan 94 14:02:48 GMT X-Mailer: mail-news 2.0.3 Lines: 43 Willi Hasselbring wrote | I used fuzz on Sun Workstations. It is a stable program. However, while | constructing specifications with fuzz I recognized an important drawback of | using Z with the fuzz package: the principle of definition before use, which | leads to a bottom-up development of the specification. It would be more | natural to write and explain the specification in a top-down manner. The | important point with Z is just that any specification must be written in a way | such that its definitions can be ordered to satisfy the principle of | definition before use (see Mike Spivey's ZRM, 2nd ed, page 47). This avoids | recursive definitions in which a schema includes itself. Therefore, it should | be possible to develop a tool for Z that allows the introduction of paragraphs | in any order and ensures that the principle of definition before use can be | satisfied. I propose a fuzz directive, which *announces* a forthcoming | definition before its use. This announcement should be invisble and it should | only include the declaration part, not the predicates. fuzz could check the | correspondence with the final definition. | | The existing fuzz directives allow preliminary, invisible definitions, but the | later final definitions cannot be type-checked because they are redefinitions | of global names. One could copy the formulae of the final definition into the | preliminary, invisible definition, but then it would become impractical to | change the specification. The issue of announce could be overcome, as in many compilers, by making fuzz a multi-pass checker. However there is a more general problem that also applies to programming languages. This is the need to generate not only a specification that can be machine checked but also a wide range of related documentation where not only the content but also the structure and order of the information should vary! This has resulted in the concept of literate programming. Various files such as documentation, technical reports, and a specification can be generated from a single source file. There are some quite simple language independent implementations of literate programming. I have used one of these (called noweb) to write formal specifications in Z which have then been type checked using fuzz. The ICL ProofPower-Z tool also uses a version of literate programming. Mike Benjamin. ___ British Aerospace Sowerby Research Centre (^v^) FPC 267, PO BOX 5, Bristol BS12 7QW, UK. / | \ Tel: (0)272 366198 Fax: (0)272 363733 --------^-^------ Email: Michael.Benjamin@src.bae.co.uk -- rbotting@wiley.csusb.edu. rbotting::=`Dr. Richard J. Botting`, wiley::=`Faculty EMail System`, csusb::=`California State University, San Bernardino, CA 92407, USA`. From rbotting@wiley.csusb.edu Wed Feb 2 18:51 PST 1994 Return-Path: Received: from wiley.csusb.edu by silicon.csci.csusb.edu (5.0/SMI-SVR4) id AA17508; Wed, 2 Feb 94 18:51:49 PST Received: by wiley.csusb.edu (5.67a/1.34) id AA08774; Wed, 2 Feb 1994 18:53:10 -0800 Date: Wed, 2 Feb 1994 18:53:10 -0800 From: rbotting@wiley.csusb.edu ("Dr. Richard Botting") Message-Id: <199402030253.AA08774@wiley.csusb.edu> To: dick@silicon.csci.csusb.edu Subject: (fwd) Re: How good is Fuzz? Newsgroups: comp.specification.z Content-Type: text Content-Length: 2526 Status: RO Newsgroups: comp.specification.z Path: csus.edu!wupost!math.ohio-state.edu!howland.reston.ans.net!pipex!uknet!comlab.ox.ac.uk!vnet.IBM.COM From: ryman@vnet.IBM.COM (Arthur Ryman) Subject: Re: How good is Fuzz? Message-ID: <19940131.112405.RYMAN@TOROLAB2> Date: 31 Jan 94 11:24:05 EST X-Mailer: mail-news 2.0.3 Comments: Resending note of Mon, 31 Jan 94 10:47:29 GMT from Lines: 33 From: Arthur Ryman *** Resending note of 01/31/94 07:37 Phone: (416) 448-3077, TIE 778-3077, FAX (416) 448-4414 ========================================================================= Wilhelm Hasselbring wrote that fuzz needs a forward reference capability. I agree in principle but this touches on a deeper issue in the design of Z. Z requires that a spec have an ordering that eliminates circular definitions. Tools like fuzz enforce this by requiring that the spec be written in def-before-use order. Tools like the IBM ZTOOLS, which I mainly use, do not require def-before-use. Def-before-use has the advantage of giving the reader a warm feeling since nothing is pulled out of thin air. However, it is awkward to use in a top-down refinement style of presentation. For example, I may want to describe a system that consists of some subsystems. When I introduce the system, I want to give the reader the big picture and not burden him with the details of the subsystems. It might be enough to say that each subsystem has an associated type. To describe the system, all I need to use about the subsystems is that I can declare variables to name them, form sets of them, etc. I think it would be very useful if Z allowed me to simply say that some new name represents a type, and later I'll tell you if I'm defining it as a given set, schema, or cartesian product type. The new name would have the same status as a formal parameter to a generic type, until it was defined, i.e. I could introduce a type name and later refine it into a concrete type. Note that this is only a problem for types since one can use axiomatic definitions to introduce variable names which can later be further constrained through the use of predicates, e.g. introduce the name max_people : Z on page 1 and say max_people > 100 and page 20. Why not allow one to introduce the type Client : Type on page 1 and say Client is a given set [Client] (or a schema or a product) on page 20? -- rbotting@wiley.csusb.edu. rbotting::=`Dr. Richard J. Botting`, wiley::=`Faculty EMail System`, csusb::=`California State University, San Bernardino, CA 92407, USA`. From rbotting@wiley.csusb.edu Sat Feb 5 20:31 PST 1994 Return-Path: Received: from wiley.csusb.edu by silicon.csci.csusb.edu (5.0/SMI-SVR4) id AA25671; Sat, 5 Feb 94 20:31:38 PST Received: by wiley.csusb.edu (5.67a/1.34) id AA03422; Sat, 5 Feb 1994 20:32:51 -0800 Date: Sat, 5 Feb 1994 20:32:51 -0800 From: rbotting@wiley.csusb.edu ("Dr. Richard Botting") Message-Id: <199402060432.AA03422@wiley.csusb.edu> To: dick@silicon.csci.csusb.edu Subject: (fwd) Availability of Fuzz Newsgroups: comp.specification.z Content-Type: text Content-Length: 770 Status: RO Path: csus.edu!wupost!cs.utexas.edu!howland.reston.ans.net!europa.eng.gtefsd.com!news.umbc.edu!eff!news.kei.com!ub!newserve!bingsuns.cc.binghamton.edu!not-for-mail From: madhav@bingsuns.cc.binghamton.edu (madhav) Newsgroups: comp.specification.z Subject: Availability of Fuzz Date: 31 Jan 1994 17:11:49 -0500 Organization: Binghamton University, Binghamton, NY Lines: 6 Message-ID: <2ijvn5$1hd@bingsuns.cc.binghamton.edu> References: <1994Jan25.102706.14386@def.bae.co.uk> NNTP-Posting-Host: bingsuns-gw.cc.binghamton.edu Is Fuzz (the Z type checker) available over the net? Thanks, Neel Madhav. -- rbotting@wiley.csusb.edu. rbotting::=`Dr. Richard J. Botting`, wiley::=`Faculty EMail System`, csusb::=`California State University, San Bernardino, CA 92407, USA`. From rbotting@wiley.csusb.edu Sat Feb 5 20:32 PST 1994 Return-Path: Received: from wiley.csusb.edu by silicon.csci.csusb.edu (5.0/SMI-SVR4) id AA25676; Sat, 5 Feb 94 20:32:12 PST Received: by wiley.csusb.edu (5.67a/1.34) id AA03439; Sat, 5 Feb 1994 20:33:26 -0800 Date: Sat, 5 Feb 1994 20:33:26 -0800 From: rbotting@wiley.csusb.edu ("Dr. Richard Botting") Message-Id: <199402060433.AA03439@wiley.csusb.edu> To: dick@silicon.csci.csusb.edu Subject: (fwd) Z in HOL Newsgroups: comp.specification.z Content-Type: text Content-Length: 1128 Status: RO Newsgroups: comp.specification.z Path: csus.edu!netcom.com!netcomsv!decwrl!elroy.jpl.nasa.gov!usc!howland.reston.ans.net!pipex!uknet!comlab.ox.ac.uk!comlab.oxford.ac.uk From: Mike.Gordon@computer-lab.cambridge.ac.uk Subject: Z in HOL Message-ID: <9402011131.AA12267@topaz.comlab.ox.ac.uk> Date: Tue, 1 Feb 94 11:31:53 GMT X-Mailer: mail-news 2.0.3 Lines: 19 An experimental prototype shallow embedding of (part of) the Z specification notation in HOL88 is available by anonymous ftp: Site: ftp.cl.cam.ac.uk [128.232.0.56] Directory: hvg/contrib/Z File: READ-ME This requires HOL88 Version 2.02 (though a patch for AKCL Version 2.01 will load automatically). The prototype is liable to change, possibly drastically. It is based on joint work with Jonathan Bowen of Oxford. Mike Gordon P.S Serious users of Z are reminded that an industrial strength embedding of Z in HOL is available from ICL (ProofPower-server@win.icl.co.uk). -- rbotting@wiley.csusb.edu. rbotting::=`Dr. Richard J. Botting`, wiley::=`Faculty EMail System`, csusb::=`California State University, San Bernardino, CA 92407, USA`. From rbotting@wiley.csusb.edu Sat Feb 5 20:33 PST 1994 Return-Path: Received: from wiley.csusb.edu by silicon.csci.csusb.edu (5.0/SMI-SVR4) id AA25680; Sat, 5 Feb 94 20:33:24 PST Received: by wiley.csusb.edu (5.67a/1.34) id AA03453; Sat, 5 Feb 1994 20:34:37 -0800 Date: Sat, 5 Feb 1994 20:34:37 -0800 From: rbotting@wiley.csusb.edu ("Dr. Richard Botting") Message-Id: <199402060434.AA03453@wiley.csusb.edu> To: dick@silicon.csci.csusb.edu Subject: (fwd) new Z textbook Newsgroups: comp.specification.z Content-Type: text Content-Length: 1552 Status: RO Newsgroups: comp.specification.z Path: csus.edu!netcom.com!netcomsv!netcomsv!amd!amdahl!pacbell.com!sgiblab!spool.mu.edu!howland.reston.ans.net!pipex!warwick!sunserver1.aston.ac.uk!cs_mac30.aston.ac.uk!user From: b.ratcliff@aston.ac.uk (bryan ratcliff) Subject: new Z textbook Message-ID: Followup-To: comp.specification.z Sender: usenet@aston.ac.uk Organization: aston university, birmingham, uk Date: Fri, 4 Feb 1994 12:29:59 GMT Lines: 31 An extremely belated HELLO to USENET and everyone interested in Z. I have just completed a textbook entitled Introducing Specification Using Z A Practical Case Study Approach which will be published by McGraw-Hill in early April (1994). The book does not break any new ground particularly, but some of you (I hope!) may find the style and price (I think it will be #17.95) more or less right. Once it's out, I'd be happy to receive any feedback about the book via Email. If you feel so inclined, mail your (polite/constructive) comments to b.ratcliff@aston.ac.uk If you want an inspection copy, post a request through to Alistair Cameron Marketing Co-ordinator McGraw-Hill Book Co. Ltd Shoppenhangers Road Maidenhead Berkshire SL6 2QL UK Look forward to hearing from you. PS Could Oxford please include the book in their bibliography etc.? -- rbotting@wiley.csusb.edu. rbotting::=`Dr. Richard J. Botting`, wiley::=`Faculty EMail System`, csusb::=`California State University, San Bernardino, CA 92407, USA`. From rbotting@wiley.csusb.edu Sat Feb 5 20:34 PST 1994 Return-Path: Received: from wiley.csusb.edu by silicon.csci.csusb.edu (5.0/SMI-SVR4) id AA25684; Sat, 5 Feb 94 20:34:35 PST Received: by wiley.csusb.edu (5.67a/1.34) id AA03461; Sat, 5 Feb 1994 20:35:48 -0800 Date: Sat, 5 Feb 1994 20:35:48 -0800 From: rbotting@wiley.csusb.edu ("Dr. Richard Botting") Message-Id: <199402060435.AA03461@wiley.csusb.edu> To: dick@silicon.csci.csusb.edu Subject: (fwd) Z fonts for Windows and Macintosh Newsgroups: comp.specification.z Content-Type: text Content-Length: 1121 Status: RO Newsgroups: comp.specification.z Path: csus.edu!uop!pacbell.com!sgiblab!spool.mu.edu!howland.reston.ans.net!pipex!uknet!comlab.ox.ac.uk!comlab.oxford.ac.uk From: zforum-request@comlab.oxford.ac.uk Subject: Z fonts for Windows and Macintosh Message-ID: <9402041355.AA22475@topaz.comlab.ox.ac.uk> Date: Fri, 4 Feb 94 13:55:28 GMT X-Mailer: mail-news 2.0.3 Lines: 14 Richard Jones has provided new Z fonts for use under MS Windows on PCs (PostScript and TrueType) and on Apple Macintosh computers. These are installed in the Z archive at Oxford as follows: Zedfont.zip.uue Z font for MS Windows (uuencoded pkzip format) 62Kbytes Zedfont.sea.hqx Z font for Apple Macintosh (BinHex 4.0 format) 116Kbytes These are available via anonymous FTP under ftp.comlab.ox.ac.uk:/Zforum or by sending the command "send z Zedfont.zip.uue" (for example) in a mail message to . -- Jonathan Bowen. Oxford University -- rbotting@wiley.csusb.edu. rbotting::=`Dr. Richard J. Botting`, wiley::=`Faculty EMail System`, csusb::=`California State University, San Bernardino, CA 92407, USA`. From rbotting@wiley.csusb.edu Fri Feb 18 16:17 PST 1994 Return-Path: Received: from wiley.csusb.edu by silicon.csci.csusb.edu (5.0/SMI-SVR4) id AA25943; Fri, 18 Feb 94 16:17:04 PST Received: by wiley.csusb.edu (5.67a/1.34) id AA19046; Fri, 18 Feb 1994 16:18:12 -0800 Date: Fri, 18 Feb 1994 16:18:12 -0800 From: rbotting@wiley.csusb.edu ("Dr. Richard Botting") Message-Id: <199402190018.AA19046@wiley.csusb.edu> To: dick@silicon.csci.csusb.edu Subject: (fwd) Re: Question: Status SSADM & Z Newsgroups: comp.specification.z Content-Type: text Content-Length: 1350 Status: RO Newsgroups: comp.specification.z Path: csus.edu!csulb.edu!library.ucla.edu!agate!doc.ic.ac.uk!uknet!titan.inmos.co.uk!dogmatix!jhr From: jhr@inmos.co.uk (Julian Rose) Subject: Re: Question: Status SSADM & Z Message-ID: <1994Feb16.085519.14262@inmos.co.uk> Sender: jhr@dogmatix (Julian Rose) Organization: INMOS Limited, Bristol, UK References: <2jr4pi$fat@news.csus.edu> Date: Wed, 16 Feb 1994 08:55:19 GMT Lines: 14 In article <2jr4pi$fat@news.csus.edu>, rbotting@wiley.csusb.edu (Dr. Richard Botting) writes: |> I heard that there was a project to form links between the UK Analysis |> and Design method - SSADM - and Z. This project was (is) called SAZ and it you may find Fiona Polack able to help you (fiona@minster.york.ac.uk) if you ask for a list of references. |> I may also have an idea for |> a research style paper on ELHs and Z. I'd like to make sure I don't |> reinvent wheels or steal thunder... (ELH = Entity Life Histories) It's hard. Your main problem is time. -- rbotting@wiley.csusb.edu. rbotting::=`Dr. Richard J. Botting`, wiley::=`Faculty EMail System`, csusb::=`California State University, San Bernardino, CA 92407, USA`. Aka::=`dick@doc.csci.csusb.edu`. Disclaimer::=`CSUSB may or may not agree with this message`. Copyright(1994)::=`Copy and use as you wish as long as you include this copywrite and signature`. From rbotting@wiley.csusb.edu Fri Feb 18 16:30 PST 1994 Return-Path: Received: from wiley.csusb.edu by silicon.csci.csusb.edu (5.0/SMI-SVR4) id AA25984; Fri, 18 Feb 94 16:30:19 PST Received: by wiley.csusb.edu (5.67a/1.34) id AA19221; Fri, 18 Feb 1994 16:31:27 -0800 Date: Fri, 18 Feb 1994 16:31:27 -0800 From: rbotting@wiley.csusb.edu ("Dr. Richard Botting") Message-Id: <199402190031.AA19221@wiley.csusb.edu> To: dick@silicon.csci.csusb.edu Subject: (fwd) Re: Question: Z and SGML Newsgroups: comp.specification.z Content-Type: text Content-Length: 1504 Status: RO Newsgroups: comp.specification.z Path: csus.edu!csulb.edu!library.ucla.edu!europa.eng.gtefsd.com!howland.reston.ans.net!pipex!logica.co.uk!mac-227.camb.logica.co.uk!user From: susan@logcam.co.uk (Susan Stepney) Subject: Re: Question: Z and SGML Message-ID: Followup-To: comp.specification.z Sender: news@carmen.logica.co.uk (News Manager Account) Nntp-Posting-Host: 158.234.41.227 Organization: Logica Cambridge References: <2jr559$fat@news.csus.edu> Date: Wed, 16 Feb 1994 17:25:29 GMT Lines: 15 In article <2jr559$fat@news.csus.edu>, rbotting@wiley.csusb.edu (Dr. Richard Botting) wrote: > > Z seems to have tools for formatting/editing/checking on several > platforms. Has any work been done on an SGML structure for documents > that contain Z statements and schemas, etc. > The Z Base Standard v 1.0 includes an SGML 'Z Interchange Format' (appendix D) ____________________________________________________________________________ Susan Stepney. susan@logcam.co.uk Logica Cambridge Ltd, Betjeman House, 104 Hills Road, Cambridge, CB2 1LQ, UK -- rbotting@wiley.csusb.edu. rbotting::=`Dr. Richard J. Botting`, wiley::=`Faculty EMail System`, csusb::=`California State University, San Bernardino, CA 92407, USA`. Aka::=`dick@doc.csci.csusb.edu`. Disclaimer::=`CSUSB may or may not agree with this message`. Copyright(1994)::=`Copy and use as you wish as long as you include this copywrite and signature`. From rbotting@wiley.csusb.edu Fri Feb 18 16:30 PST 1994 Return-Path: Received: from wiley.csusb.edu by silicon.csci.csusb.edu (5.0/SMI-SVR4) id AA25989; Fri, 18 Feb 94 16:30:53 PST Received: by wiley.csusb.edu (5.67a/1.34) id AA19232; Fri, 18 Feb 1994 16:32:01 -0800 Date: Fri, 18 Feb 1994 16:32:01 -0800 From: rbotting@wiley.csusb.edu ("Dr. Richard Botting") Message-Id: <199402190032.AA19232@wiley.csusb.edu> To: dick@silicon.csci.csusb.edu Subject: (fwd) Help: Anyone got a small test sample... Newsgroups: comp.specification.z Content-Type: text Content-Length: 1279 Status: RO Path: csus.edu!wiley!rbotting From: rbotting@wiley.csusb.edu (Dr. Richard Botting) Newsgroups: comp.specification.z Subject: Help: Anyone got a small test sample... Date: 15 Feb 1994 18:47:51 GMT Organization: California State University Sacramento Lines: 11 Message-ID: <2jr5cn$fat@news.csus.edu> NNTP-Posting-Host: wiley.csusb.edu Summary: Installation test needed Keywords: TeX Z zed.sty LaTeX X-Newsreader: TIN [version 1.2 PL2] I've just downloaded zed.sty and have been talking to the local TeX guru about it. I've got the zguide.tex as well. Can anyone suggest a small TeX file that would exercise all the fonts/goodies/etc that we might need? -- rbotting@wiley.csusb.edu. rbotting::=`Dr. Richard J. Botting`, wiley::=`Faculty EMail System`, csusb::=`California State University, San Bernardino, CA 92407, USA`. Aka::=`dick@doc.csci.csusb.edu`. Disclaimer::=`CSUSB may or may not agree with this message`. -- rbotting@wiley.csusb.edu. rbotting::=`Dr. Richard J. Botting`, wiley::=`Faculty EMail System`, csusb::=`California State University, San Bernardino, CA 92407, USA`. Aka::=`dick@doc.csci.csusb.edu`. Disclaimer::=`CSUSB may or may not agree with this message`. Copyright(1994)::=`Copy and use as you wish as long as you include this copywrite and signature`. From rbotting@wiley.csusb.edu Fri Feb 18 16:30 PST 1994 Return-Path: Received: from wiley.csusb.edu by silicon.csci.csusb.edu (5.0/SMI-SVR4) id AA25990; Fri, 18 Feb 94 16:30:54 PST Received: by wiley.csusb.edu (5.67a/1.34) id AA19236; Fri, 18 Feb 1994 16:32:02 -0800 Date: Fri, 18 Feb 1994 16:32:02 -0800 From: rbotting@wiley.csusb.edu ("Dr. Richard Botting") Message-Id: <199402190032.AA19236@wiley.csusb.edu> To: dick@silicon.csci.csusb.edu Subject: (fwd) Re: Help: Anyone got a small test sample... Newsgroups: comp.specification.z Content-Type: text Content-Length: 1470 Status: RO Newsgroups: comp.specification.z Path: csus.edu!wupost!howland.reston.ans.net!pipex!logica.co.uk!mac-227.camb.logica.co.uk!user From: susan@logcam.co.uk (Susan Stepney) Subject: Re: Help: Anyone got a small test sample... Message-ID: Followup-To: comp.specification.z Sender: news@carmen.logica.co.uk (News Manager Account) Nntp-Posting-Host: 158.234.41.227 Organization: Logica Cambridge References: <2jr5cn$fat@news.csus.edu> Date: Wed, 16 Feb 1994 17:29:45 GMT Lines: 15 In article <2jr5cn$fat@news.csus.edu>, rbotting@wiley.csusb.edu (Dr. Richard Botting) wrote: > > I've just downloaded zed.sty and have been talking to the local TeX > guru about it. I've got the zguide.tex as well. Can anyone suggest > a small TeX file that would exercise all the fonts/goodies/etc that > we might need? How about using zguide.tex? ____________________________________________________________________________ Susan Stepney. susan@logcam.co.uk Logica Cambridge Ltd, Betjeman House, 104 Hills Road, Cambridge, CB2 1LQ, UK -- rbotting@wiley.csusb.edu. rbotting::=`Dr. Richard J. Botting`, wiley::=`Faculty EMail System`, csusb::=`California State University, San Bernardino, CA 92407, USA`. Aka::=`dick@doc.csci.csusb.edu`. Disclaimer::=`CSUSB may or may not agree with this message`. Copyright(1994)::=`Copy and use as you wish as long as you include this copywrite and signature`. From rbotting@wiley.csusb.edu Fri Feb 18 16:33 PST 1994 Return-Path: Received: from wiley.csusb.edu by silicon.csci.csusb.edu (5.0/SMI-SVR4) id AA26001; Fri, 18 Feb 94 16:33:23 PST Received: by wiley.csusb.edu (5.67a/1.34) id AA19269; Fri, 18 Feb 1994 16:34:31 -0800 Date: Fri, 18 Feb 1994 16:34:31 -0800 From: rbotting@wiley.csusb.edu ("Dr. Richard Botting") Message-Id: <199402190034.AA19269@wiley.csusb.edu> To: dick@silicon.csci.csusb.edu Subject: (fwd) SSADM & Z Newsgroups: comp.specification.z Content-Type: text Content-Length: 1367 Status: RO Newsgroups: comp.specification.z Path: csus.edu!uop!pacbell.com!ames!elroy.jpl.nasa.gov!swrinde!cs.utexas.edu!howland.reston.ans.net!pipex!uknet!comlab.ox.ac.uk!teesside.ac.uk From: zoro@teesside.ac.uk (Z forum (cmr24/cmr23/cms05)) Subject: SSADM & Z Message-ID: <3511.9402161545@hector> Date: Wed, 16 Feb 94 15:45:24 GMT X-Mailer: mail-news 2.0.3 Lines: 23 rbotting@edu.csusb.wiley writes: | I heard that there was a project to form links between the UK Analysis | and Design method - SSADM - and Z. ?? York University's SAZ (SSADM & Z) project. | I was wondering about how this was going. I was involved in SSADM | at its birth (I boiled the water you might say :-)) and have always | had a strong interest in formal methods. I may also have an idea for | a research style paper on ELHs and Z. I'd like to make sure I don't | reinvent wheels or steal thunder... It was launched as a method in January this year. For more info you could try liz@minster.york.ac.uk. regards, Andy Galloway. -- rbotting@wiley.csusb.edu. rbotting::=`Dr. Richard J. Botting`, wiley::=`Faculty EMail System`, csusb::=`California State University, San Bernardino, CA 92407, USA`. Aka::=`dick@doc.csci.csusb.edu`. Disclaimer::=`CSUSB may or may not agree with this message`. Copyright(1994)::=`Copy and use as you wish as long as you include this copywrite and signature`. From georgiou@silicon.csci.csusb.edu Sun Apr 3 19:33 PDT 1994 Return-Path: Received: from blaze.csci.csusb.edu by silicon.csci.csusb.edu (5.0/SMI-SVR4) id AA11514; Sun, 3 Apr 94 19:33:39 PDT Received: from silicon.csci.csusb.edu by blaze.csci.csusb.edu (AIX 3.2/UCB 5.64/4.03) id AA29547; Sun, 3 Apr 1994 18:05:11 -0800 Received: from orion.csci.csusb.edu by silicon.csci.csusb.edu (5.0/SMI-SVR4) id AA11511; Sun, 3 Apr 94 19:33:14 PDT Received: by orion.csci.csusb.edu (5.0/SMI-SVR4) id AA06286; Sun, 3 Apr 94 19:29:11 PDT Date: Sun, 3 Apr 94 19:33:14 PDT Message-Id: <9404040233.AA11511@silicon.csci.csusb.edu> To: dick@blaze.csci.csusb.edu Subject: zed Return-Receipt-To: georgiou@silicon.csci.csusb.edu From: georgiou@silicon.csci.csusb.edu Content-Type: text Content-Length: 509 Status: RO After > 3hrs of detective work, I've located and installed in the appropriate places the ams fonts needed by zed on blaze. The file /u/class/georgiou/zguide.ps is the postscript version of zguide.tex. There were no complaints about missing fonts, and thus all symbols should print ok. In case the zed option in latex (zed.sty) doesn't work properly for you, my guess is that an environment variable(s) must be set, such as TEXFONTS. But I feel that this won't be needed, but please let me know. --George From rbotting@wiley.csusb.edu Wed Apr 6 14:30 PDT 1994 Return-Path: Received: from wiley.csusb.edu by silicon.csci.csusb.edu (5.0/SMI-SVR4) id AA23507; Wed, 6 Apr 94 14:29:55 PDT Received: by wiley.csusb.edu (5.67a/1.34) id AA13676; Wed, 6 Apr 1994 14:30:22 -0700 Date: Wed, 6 Apr 1994 14:30:22 -0700 From: rbotting@wiley.csusb.edu ("Dr. Richard Botting") Message-Id: <199404062130.AA13676@wiley.csusb.edu> To: dick@silicon.csci.csusb.edu Subject: (fwd) ZTC: A Z Type Checker (version 1.3) Newsgroups: comp.specification.z Content-Type: text Content-Length: 1519 Status: RO Newsgroups: comp.specification.z Path: csus.edu!wupost!darwin.sura.net!howland.reston.ans.net!vixen.cso.uiuc.edu!usenet.ucs.indiana.edu!depaul!hawk!cscjx From: cscjx@hawk.depaul.edu (Jia Xiaoping) Subject: ZTC: A Z Type Checker (version 1.3) Nntp-Posting-Host: hawk.depaul.edu Sender: news@hal.depaul.edu (News Admin) Organization: DePaul University, Chicago Il. Date: Wed, 6 Apr 1994 20:14:34 GMT Message-ID: <1994Apr6.201434.14161@hal.depaul.edu> Lines: 21 A new version of ZTC is now available. It runs on IBM-PC and Sun SPARC workstations. It can be obtained via anonymous ftp at Address: ise.cs.depaul.edu (140.192.32.117) User name: ftp Password: your e-mail address Directory: /dist You will find the following files in the directory: ZTC-1.3-DOS.tar.Z MS-DOS version for IBM-PC ZTC-1.3-Sun4.tar.Z Sun SPARC version for SunOS 4.x ZTC-1.3-Solaris.tar.Z Sun SPARC version for Solaris 2.x readme this file For the PC version, you have to uncompress and untar the file on a UNIX system, then download the files to your PC. All files except ZTC.EXE are ASCII files. -- rbotting@wiley.csusb.edu. rbotting::=`Dr. Richard J. Botting`, wiley::=`Faculty EMail System`, csusb::=`California State University, San Bernardino, CA 92407, USA`. Aka::=`dick@doc.csci.csusb.edu`. Disclaimer::=`CSUSB may or may not agree with this message`. Copyright(1994)::=`Copy and use as you wish as long as you include this copyright and signature`. Ask me about our new Masters degree in Computer Science! From rbotting@wiley.csusb.edu Fri May 13 13:43 PDT 1994 Return-Path: Received: from wiley.csusb.edu by silicon.csci.csusb.edu (5.0/SMI-SVR4) id AA08195; Fri, 13 May 94 13:43:28 PDT Received: by wiley.csusb.edu (5.67a/1.34) id AA18445; Fri, 13 May 1994 13:43:32 -0700 From: rbotting@wiley.csusb.edu ("Dr. Richard Botting") Message-Id: <199405132043.AA18445@wiley.csusb.edu> Subject: Style and Z To: dick@silicon.csci.csusb.edu Date: Fri, 13 May 1994 13:43:32 -0700 (PDT) X-Mailer: ELM [version 2.4 PL22] Content-Type: text Content-Length: 2431 Status: RO Received: by wiley.csusb.edu (5.67a/1.34) id AA25923; Mon, 9 May 1994 13:12:40 -0700 Date: Mon, 9 May 1994 13:12:40 -0700 From: rbotting ("Dr. Richard Botting") Message-Id: <199405092012.AA25923@wiley.csusb.edu> To: dick@silicon.csci.csusb.edu Subject: (fwd) Re: A question about style (or a problem with Z?) Newsgroups: daniel.jackson@cs.cmu.edu Newsgroups: comp.specification.z Path: csus.edu!wupost!gumby!newsxfer.itd.umich.edu!zip.eecs.umich.edu!panix!MathWorks.Com!noc.near.net!das-news.harvard.edu!honeydew.srv.cs.cmu.edu!BEMBO.SP.CS.CMU.EDU!dnj From: dnj+@CS.CMU.EDU (Daniel Jackson) Subject: Re: A question about style (or a problem with Z?) Message-ID: Followup-To: daniel.jackson@cs.cmu.edu Keywords: frame conditions Sender: news@cs.cmu.edu (Usenet News System) Nntp-Posting-Host: bembo.sp.cs.cmu.edu Organization: Carnegie Mellon University References: Date: Fri, 6 May 1994 15:40:02 GMT Lines: 30 Phil Stocks's response to Linda Pazzaglia is right: you can't write f'(a) = b if what you mean is f' = f (+) {a |-> b} because the assertion is not an assignment. But let's not dismiss this so quickly. You have to say that f is unchanged elsewhere because there's no frame condition that would allow this to be inferred. This makes reasoning simpler, but it prevents a desirable kind of composition. Suppose f represents Spivey's birthday book, and I want to define an operation that enters the birthdays of two friends who are married: wife_name?, husband_name?: Name wife_date?, husband_date?: Date Why not just promote the operation for entering individual birthdays twice and conjoin the instances? Z won't let you do this, of course, and you would be forced instead to define the operation from scratch, or perhaps use sequential composition (thus introducing an ugly bias). Daniel Jackson School of Computer Science Carnegie Mellon University -- rbotting@wiley.csusb.edu. rbotting::=`Dr. Richard J. Botting`, wiley::=`Faculty EMail System`, csusb::=`California State University, San Bernardino, CA 92407, USA`. Aka::=`dick@doc.csci.csusb.edu`. Disclaimer::=`CSUSB may or may not agree with this message`. Copyright(1994)::=`Copy and use as you wish as long as you include this copyright and signature`. Send EMail to gradinfo@silicon.csci.csusb.edu for info on a new Masters degree in Computer Science! From rbotting@wiley.csusb.edu Fri May 13 13:46 PDT 1994 Return-Path: Received: from wiley.csusb.edu by silicon.csci.csusb.edu (5.0/SMI-SVR4) id AA08244; Fri, 13 May 94 13:46:41 PDT Received: by wiley.csusb.edu (5.67a/1.34) id AA22832; Fri, 13 May 1994 13:46:46 -0700 From: rbotting@wiley.csusb.edu ("Dr. Richard Botting") Message-Id: <199405132046.AA22832@wiley.csusb.edu> Subject: Process boks To: dick@silicon.csci.csusb.edu Date: Fri, 13 May 1994 13:46:46 -0700 (PDT) X-Mailer: ELM [version 2.4 PL22] Content-Type: text Content-Length: 4564 Status: RO Path: csus.edu!csulb.edu!nic-nac.CSU.net!usc!howland.reston.ans.net!pipex!doc.ic.ac.uk!usenet From: ban@doc.ic.ac.uk (Bashar Nuseibeh) Newsgroups: comp.specification Subject: New book on Process Modelling and Technology Date: 9 May 1994 17:44:47 GMT Organization: Imperial College, Dept. of Computing Lines: 97 Distribution: world Message-ID: <2qlsqf$m47@frigate.doc.ic.ac.uk> NNTP-Posting-Host: dse-mac-bashar.doc.ic.ac.uk You may want to pass on the details of the new book below to your library. --------------------------- cut here ----------------------------- Software Process Modelling and Technology Edited by A. Finkelstein, J. Kramer and B. Nuseibeh This book provides an account of the key European contributions to the international community of researchers in software process modelling and technology. The projects selected reflect the range of issues within the field; as such, the book form a valuable resource for researchers and practitioners seeking to establish the "state of the art". The book begins with a brief introduction to process-centred environments and then proposes a conceptual framework for describing and assessing evolving software processes. In the core of the book, ten projects which address different software process modelling and technology issues are described. These are: EPOS, SOCCA, MERLIN, OIKOS, ALF, ADELE-TEMP, SPADE, PEACE, E3, and PADM. The concluding chapter provides and experimental assessment exercise that compares and evaluates the different projects according to a list of assessment criteria. Contents: An Introduction to Process-Centred Environments; Concepts for Evolving Software Processes; EPOS: Object-Oriented Cooperative Process Modelling; SOCCA: Specifications of Coordinated and Cooperative Activities; MERLIN: Supporting Cooperation in Software Development through a Knowledge-Based Environment; OIKOS: Constructing Process-Centred SDEs; ALF: A Framework for Building Process-Centred Software Engineering Environments; ADELE-TEMPO: An Environment to Support Process Modelling and Enaction; SPADE: An Environment for Software Process Analysis, Design and Enactment; PEACE: Goal-Oriented Logic-Based Formalism for Process Modelling; E3: Object-Oriented Software Process Model Design; PADM: Towards a Total Process Modelling System; An Assessment Exercise; Index. 0 86380 169 2 384pp UK Pds 47.50/US $78.50 Research Studies Press (distributed by Wiley) ----------------- ORDER FORM ----------------------------------- Please send me _____ cop(ies) of: FINKELSTEIN/Software 0 86380 169 2 UK Pds 47.50/US $78.50 Please add UK Pds 2.00/US $5.00 to cover postage __ I enclose a cheque/bank draft for __________ (payable to John Wiley & Sons Ltd.) __ Please charge my credit card account __ Mastercard __ American Express __ Barclaycard/Visa __ Diners Club __ JCB Card Number: ___________________________ Expiry Date: _______________ [ ] Please send and invoice [ ] I do not wish to receive mail from other companies You may telephone your credit card order by dialling Linkline 0800 243407 (UK only). We will refund your payment without question if you return any unwanted book to us in re-saleable condition within 30 days Your order will be dispatched promptly but please allow 21 days for delivery. Prices correct at the time of printing but subject to change. IMPORTANT - EC countries please complete details below. [ ] I am registered for VAT, my VAT registration number is ______________________ [ ] I am exempt from VAT and enclose proof. If registered for VAT, please quote you VAT number above. For non-registered customers, it may be necessary to add VAT to your order. PLEASE PRINT Name ___________________________________ Address ___________________________________ ___________________________________ ___________________________________ ___________________________________ ___________________________________ Signature _____________________ Date _________ RETURN TO: Nikki Phillips, John Wiley and Sons Ltd., Baffins Lane, Chichester, West Sussex, PO19 1UD, UK. -- rbotting@wiley.csusb.edu. rbotting::=`Dr. Richard J. Botting`, wiley::=`Faculty EMail System`, csusb::=`California State University, San Bernardino, CA 92407, USA`. Aka::=`dick@doc.csci.csusb.edu`. Disclaimer::=`CSUSB may or may not agree with this message`. Copyright(1994)::=`Copy and use as you wish as long as you include this copyright and signature`. Send EMail to gradinfo@silicon.csci.csusb.edu for info on a new Masters degree in Computer Science! From rbotting@wiley.csusb.edu Fri May 13 13:45 PDT 1994 Return-Path: Received: from wiley.csusb.edu by silicon.csci.csusb.edu (5.0/SMI-SVR4) id AA08208; Fri, 13 May 94 13:45:12 PDT Received: by wiley.csusb.edu (5.67a/1.34) id AA20797; Fri, 13 May 1994 13:45:17 -0700 From: rbotting@wiley.csusb.edu ("Dr. Richard Botting") Message-Id: <199405132045.AA20797@wiley.csusb.edu> Subject: Style and Z To: dick@silicon.csci.csusb.edu Date: Fri, 13 May 1994 13:45:17 -0700 (PDT) X-Mailer: ELM [version 2.4 PL22] Content-Type: text Content-Length: 2477 Status: RO Path: csus.edu!csulb.edu!nic-nac.CSU.net!usc!howland.reston.ans.net!agate!msuinfo!harbinger.cc.monash.edu.au!bunyip.cc.uq.oz.au!uqcspe.cs.uq.oz.au!cs.uq.oz.au!brendan From: brendan@cs.uq.oz.au (Brendan Mahony) Newsgroups: comp.specification.z Subject: Re: A question about style (or a problem with Z?) Date: 9 May 1994 05:00:12 GMT Organization: Computer Science Dept, University of Queensland Lines: 44 Distribution: world Message-ID: <2qkg0s$apn@uqcspe.cs.uq.oz.au> References: <2qgc0c$8i9@cybernet.cse.fau.edu> Reply-To: brendan@cs.uq.oz.au NNTP-Posting-Host: snail.cs.uq.oz.au Keywords: frame conditions The discussion seems to be: 1 Simply specifying the action on the function value being updated leaves the behaviour of the rest of the function undefined. 2 Defining the behaviour on the rest of the function means that a multiple update operator cannot be defined by modifying the single update version. Simple solution: Define the multiple updator first and specialise to single updator. ie define operator to change a collection of values, then specialise to singleton or doubleton. Complex solution: Split specification into an update operation and an operation that keeps the rest stable. +--Stable----------------- | Index, Index' : Key \fun Data | UpdateSet : \power Key +---------------- | \forall k : Key \setminus UpdateSet \spot | Index'(k) = Index(k) +------------------------- +--SingleUpdate----------- | Index, Index' : Key \fun Data | k? : Key | d? : Data +---------------- | Index'(k?) = d +------------------------- DoubleUpdate \defs SingleUpdate[k?\k1?,d?\d1?] /\ SingleUpdate[k?\k2?,d?\d2?] SingleOp \defs (SingleUpdate /\ Stable /\ UpdateSet={k?}) \hide UpdateSet DoubleOp \defs (DoubleUpdate /\ Stable /\ UpdateSet={k1?,k2?}) \hide UpdateSet Personally, I don't see much to recommend the second solution over the first. -- rbotting@wiley.csusb.edu. rbotting::=`Dr. Richard J. Botting`, wiley::=`Faculty EMail System`, csusb::=`California State University, San Bernardino, CA 92407, USA`. Aka::=`dick@doc.csci.csusb.edu`. Disclaimer::=`CSUSB may or may not agree with this message`. Copyright(1994)::=`Copy and use as you wish as long as you include this copyright and signature`. Send EMail to gradinfo@silicon.csci.csusb.edu for info on a new Masters degree in Computer Science! From rbotting@wiley.csusb.edu Thu May 26 12:39 PDT 1994 Return-Path: Received: from wiley.csusb.edu by silicon.csci.csusb.edu (5.0/SMI-SVR4) id AA06294; Thu, 26 May 94 12:39:52 PDT Received: by wiley.csusb.edu (5.67a/1.34) id AA11265; Thu, 26 May 1994 12:39:47 -0700 Date: Thu, 26 May 1994 12:39:47 -0700 From: rbotting@wiley.csusb.edu ("Dr. Richard Botting") Message-Id: <199405261939.AA11265@wiley.csusb.edu> To: dick@silicon.csci.csusb.edu Subject: (fwd) PROBLEMS WITH PIPE Newsgroups: comp.specification.z Content-Type: text Content-Length: 2383 Status: RO Newsgroups: comp.specification.z Path: csus.edu!uop!pacbell.com!ihnp4.ucsd.edu!swrinde!cs.utexas.edu!math.ohio-state.edu!jussieu.fr!univ-lyon1.fr!ghost.dsi.unimi.it!dm.unibo.it!cs.unibo.it!abarbier From: abarbier@cs.unibo.it (Andrea Barbieri) Subject: PROBLEMS WITH PIPE Message-ID: Sender: news@dm.unibo.it Organization: Laboratory for Computer Science, University of Bologna, Italy Date: Tue, 24 May 1994 14:47:00 GMT Lines: 68 I'm a student from the university of Bologna (Italy). I would be glad to get some information about piping's semantics (>>). Given two schemas composed by piping, how is generated the signature and predicative part? I feel that the semantics described in some references is not clear. I'm especially interested in these particular examples: given these state's and operation's schemas ----State------------------ | s1,s2: N --------------------------- | s1 > s2 --------------------------- ----XiSchema--------------- | State | State' | inout!: N --------------------------- | s1'=s1 | s2'=s2 | inout!=s1+1 --------------------------- ----DeltaSchema1----------- | State | State' | inout?: N --------------------------- | s1'=inout? --------------------------- ----DeltaSchema2----------- | State | State' | inout!: N --------------------------- | inout!=s2-1 | s2'=s2-1 --------------------------- ----Check------------------ | inout!,inout?: N --------------------------- | inout?>0 | | inout!=inout? -------------------------- are the following operations possible and what are their result schemas? 1) XiSchema >> DeltaSchema1 2) DeltaSchema2 >> DeltaSchema1 3) XiSchema >> Check >> DeltaSchema1 4) DeltaSchema2 >> Check >> DeltaSchema1 Please reply directly to my email address. Thanks Andrea ______________________ Barbieri Andrea email: abarbier@unibo.cs.it University of Bologna Bologna Italy -- rbotting@wiley.csusb.edu. rbotting::=`Dr. Richard J. Botting`, wiley::=`Faculty EMail System`, csusb::=`California State University, San Bernardino, CA 92407, USA`. Aka::=`dick@doc.csci.csusb.edu`. Disclaimer::=`CSUSB may or may not agree with this message`. Copyright(1994)::=`Copy and use as you wish as long as you include this copyright and signature`. Send EMail to gradinfo@silicon.csci.csusb.edu for info on a new Masters degree in Computer Science! From rbotting@wiley.csusb.edu Thu May 26 12:41 PDT 1994 Return-Path: Received: from wiley.csusb.edu by silicon.csci.csusb.edu (5.0/SMI-SVR4) id AA06306; Thu, 26 May 94 12:41:16 PDT Received: by wiley.csusb.edu (5.67a/1.34) id AA11283; Thu, 26 May 1994 12:41:11 -0700 Date: Thu, 26 May 1994 12:41:11 -0700 From: rbotting@wiley.csusb.edu ("Dr. Richard Botting") Message-Id: <199405261941.AA11283@wiley.csusb.edu> To: dick@silicon.csci.csusb.edu Subject: (fwd) Re: egg or hen? Newsgroups: comp.specification.z Content-Type: text Content-Length: 3067 Status: RO Path: csus.edu!csulb.edu!nic-nac.CSU.net!usc!cs.utexas.edu!howland.reston.ans.net!spool.mu.edu!news.clark.edu!netnews.nwnet.net!news.u.washington.edu!news.u.washington.edu!jon From: jon@bilbo.radonc.washington.edu (Jon Jacky) Newsgroups: comp.specification.z Subject: Re: egg or hen? Date: 25 May 94 09:00:28 Organization: /users/jon/.organization Lines: 73 Message-ID: References: <9405171147.AA10318@london.informatik.uni-stuttgart.de> NNTP-Posting-Host: bilbo.radonc.washington.edu In-reply-to: li@bruessel.informatik.uni-stuttgart.d400.de's message of Tue, 17 May 1994 13:47:02 +0200 In article <9405171147.AA10318@london.informatik.uni-stuttgart.de> li@bruessel.informatik.uni-stuttgart.d400.de (li jinhua) writes: > I come across a difficulty by using Z to define two shemas which > directly use each other. The notation for free type definitions of Z > can solve recursive structures, but I am not sure if it can be used to > describe indirect recursive. ... > > Problem: In a hierarchical graphical system, I want to define two > objects, an Module and a Sheet. An module is a template which > consists of an interface and a sheet. ... This sounds similar to the problem that arises when you want to describe a network of some kind. This approach does *not* work: +-- Node ------ | contents: ... | links: P Node | ... +-------------- +-- Network --- | nodes: P Node | ... +-------------- This is *not* Z because the definition of Node refers to itself. The solution is to describe the nodes and the connections between them separately. The network is just a relation on Node: +-- Node ------ | contents: ... | ... +-------------- +-- Network --- | nodes: Node <-> Node | ... +-------------- This is often clearer and more natural anyway. The links are really just a way to implement the network. If you want to express the links in Z, you could do it by defining a new basic type of identifiers ID such that every Node contains a unique ID. Then the links are sets of ID, not sets of Node, so there is no recursion. [ID] +-- Node ----- | id: ID | contents: ... | links: P ID | ... +------------- +-- Network ---- | nodes: P Node | ... +--------------- The predicates in Network would say that every Node in Network has a unique ID, and every ID in a link identifies some Node that is in Network. - Jon -- Jonathan Jacky jon@radonc.washington.edu Radiation Oncology RC-08 voice: (206)-548-4117 University of Washington FAX: (206)-548-6218 Seattle, Washington 98195 USA -- rbotting@wiley.csusb.edu. rbotting::=`Dr. Richard J. Botting`, wiley::=`Faculty EMail System`, csusb::=`California State University, San Bernardino, CA 92407, USA`. Aka::=`dick@doc.csci.csusb.edu`. Disclaimer::=`CSUSB may or may not agree with this message`. Copyright(1994)::=`Copy and use as you wish as long as you include this copyright and signature`. Send EMail to gradinfo@silicon.csci.csusb.edu for info on a new Masters degree in Computer Science!