From nic.csu.net!usc!howland.reston.ans.net!gatech!destroyer!cs.ubc.ca!uw-beaver!sullivan Mon May 17 08:54:35 1993 Relay-Version: VMS News - V6.1B5 17/9/92 VAX/VMS V5.5-2; site nic.csu.net Path: nic.csu.net!usc!howland.reston.ans.net!gatech!destroyer!cs.ubc.ca!uw-beaver!sullivan Newsgroups: comp.specification.z Subject: Shortcomings of Z? Message-ID: <1993May11.183115.4716@beaver.cs.washington.edu> From: sullivan@cs.washington.edu (Kevin Sullivan) Date: Tue, 11 May 93 18:31:15 GMT Sender: news@beaver.cs.washington.edu (USENET News System) Organization: Computer Science & Engineering, U. of Washington, Seattle Lines: 13 Status: O Very briefly, what are the most critical "shortcomings" of Z? (I understand one person's shortcoming may be another's strength.) Here's a list for starters. What should I add, if anything? 1. Monomorphic type system 2. No explicit support for specifying concurrency -- Kevin Sullivan Department of Computer Science and Engineering, FR-35 University of Washington Seattle, WA 98195 From nic.csu.net!usc!howland.reston.ans.net!darwin.sura.net!haven.umd.edu!uunet!walter!porthos!dancer!haim Mon May 17 08:54:36 1993 Relay-Version: VMS News - V6.1B5 17/9/92 VAX/VMS V5.5-2; site nic.csu.net Path: nic.csu.net!usc!howland.reston.ans.net!darwin.sura.net!haven.umd.edu!uunet!walter!porthos!dancer!haim Newsgroups: comp.specification.z Subject: Re: Shortcomings of Z? Message-ID: <1993May11.225038.26107@porthos.cc.bellcore.com> From: haim@dancer.cc.bellcore.com (kilov,haim) Date: Tue, 11 May 93 22:50:38 GMT Sender: netnews@porthos.cc.bellcore.com (USENET System Software) References: <1993May11.183115.4716@beaver.cs.washington.edu> Organization: Bellcore, Livingston, NJ Lines: 6 Status: O Add quite weak facilities for specifying generic reusable classes, including associations. This includes "structured" formal parameters. Object Z helps in providing (isolated) class schemas, but they need to be extended. -Haim Kilov haim@bcr.cc.bellcore.com From nic.csu.net!csus.edu!wupost!howland.reston.ans.net!torn!nott!bnrgate!bnr.co.uk!uknet!zaphod.axion.bt.co.uk!fmg!pky Mon May 17 08:54:36 1993 Relay-Version: VMS News - V6.1B5 17/9/92 VAX/VMS V5.5-2; site nic.csu.net Path: nic.csu.net!csus.edu!wupost!howland.reston.ans.net!torn!nott!bnrgate!bnr.co.uk!uknet!zaphod.axion.bt.co.uk!fmg!pky Newsgroups: comp.specification.z Subject: Re: Shortcomings of Z? Message-ID: <1993May12.102836.3306@fmg.bt.co.uk> From: pky@fmg.bt.co.uk (Pete Young) Date: Wed, 12 May 93 10:28:36 GMT References: <1993May11.183115.4716@beaver.cs.washington.edu> Organization: British Telecom X-Newsreader: Tin 1.1 PL5 Lines: 9 Status: O Kevin Sullivan (sullivan@cs.washington.edu) wrote: : Here's a list for starters. What should I add, if anything? No facility for specifying additional operators for the schema calculus. -- ____________________________________________________________________ Pete Young pky@fmg.bt.co.uk Phone +44 473 227151 "Most people prefer entertaining nonsense to unexciting reality" From root Thu May 20 09:00:14 1993 Received: from xrly.eng.cam.ac.uk by silicon.csci.csusb.edu (AIX 3.2/UCB 5.64/4.03) id AA22291; Thu, 20 May 1993 09:00:10 -0700 From: Peter T. Breuer Message-Id: <7421.9305201614@club.eng.cam.ac.uk> Subject: Re: Z spec generating C code To: dick@silicon.csci.csusb.edu (Dr. Richard Botting) (Dr. Richard Botting) Date: Thu, 20 May 93 17:14:53 BST In-Reply-To: <9305201523.AA15985@silicon.csci.csusb.edu>; from "Dr. Richard Botting" at May 20, 93 8:23 am X-Anonymously-To: Mailer: Elm [revision: 70.30] Status: RO > > > > just perfect as an implementation! > I prefer > main(){while(1);} Yep. better. > To be more serious this is only a zero-th approximation to say the > Halting problem. Also a zero-th approx to *all* other problems too. > (hum including acker(200)!) That all of Z is executable (to varying degrees0 is expressed in a paper of mine, which I would be glad to loan you a postscript copy of, sometime tomorrow, say (the machines are going down for maintenance). The idea is that set theory is too concrete to be executable, and that one has to take an executable _abstraction_ before one gets anywhere. The paper sets up a mechanism for doing executable implementations (there are lots) and proving them correct. And it does one, and proves it correct - and maximal in some senses. > I guess we can construct a space of specifications using > the maximum number of steps over which the code gives the > correct answer to set up a Dana Scott style Domain or > a Metric space so that the sequence of specs converge to > the ideal spec. Sort of. > In this space, your code is a long way from being perfect. Oh yes, except for problems like checking whether Peano arithmetic is a consistent system. > But then I suppose *all* the approximations are an infinite > distance from the ideal if we take a different metric. Metrics don't have infinities in them! > dick::="Dr. Richard John Botting". > csusb::="California State University, San Bernardino". > dick@silicon.csci.csusb.edu=dick@silicon.csusb.edu=rbotting@wiley.csusb.edu. > Cookie::="If god had wanted me to use UNIX I wouldn't have 10 thumbs.". Hic. -- Peter T. Breuer From nic.csu.net!csus.edu!wupost!cs.utexas.edu!uunet!pipex!uknet!comlab.ox.ac.uk!cookie.enet.dec.com Mon May 24 11:23:56 1993 Relay-Version: VMS News - V6.1B5 17/9/92 VAX/VMS V5.5-2; site nic.csu.net Path: nic.csu.net!csus.edu!wupost!cs.utexas.edu!uunet!pipex!uknet!comlab.ox.ac.uk!cookie.enet.dec.com Newsgroups: comp.specification.z Subject: Re: Z spec generating C code Message-ID: <9305201408.AA18558@enet-gw.pa.dec.com> From: wallace@cookie.enet.dec.com ("Richard Wallace, CX02-1/7A, DTN:522-2792 20-May-1993 0806") Date: Thu, 20 May 93 07:08:44 PDT X-Mailer: mail-news 2.0.3 Lines: 29 Status: O Dr. Botting of CSU, San Bernardio, CA, U.S.A writes: |If such a tool exists then it is either incomplete or it is in error since |it is possible to specify problems in Z that are not computable. Care to elaborate? I can see your point where you can have mappings of a specification to an incomplete mathematical system. That is to say the "Incompletedness" problem where one can specify that {x:Z * x :1/x} where 1/0 is not defined and thus by our incomplete mathematical system is "noncomputable." Such pitfalls can be avoided by a source code generation system if current compiler optimization technology is applied. Talk to anybody who has created an Ada compiler about range constraint violation checking during static semantic analysis and you'll lean that these issues can be forseen. Thus the tool may not be generating errors, but may be only able to do limited (read as "cheap or sloppy") static semantic analysis. Richard Wallace Senior Software Engineer Digital Equipment Corporation 301 Rockrimmon Blvd. South CXO2-1/7A Colorado Springs, CO 80919-2398 (719)548-2792 "The opinions expressed are my own, B.P. may not *quite* agree..." From nic.csu.net!csus.edu!wupost!uunet!pipex!uknet!pavo.csi.cam.ac.uk!jg Mon May 24 11:23:57 1993 Relay-Version: VMS News - V6.1B5 17/9/92 VAX/VMS V5.5-2; site nic.csu.net Path: nic.csu.net!csus.edu!wupost!uunet!pipex!uknet!pavo.csi.cam.ac.uk!jg Newsgroups: comp.specification.z Subject: Re: Z spec generating C code Message-ID: <1993May20.145012.16431@infodev.cam.ac.uk> From: jg@cl.cam.ac.uk (Jim Grundy) Date: Thu, 20 May 1993 14:50:12 GMT Reply-To: jg@cl.cam.ac.uk Sender: news@infodev.cam.ac.uk (USENET news) References: <9305201408.AA18558@enet-gw.pa.dec.com> Organization: Cambridge Hardware Verification Group Nntp-Posting-Host: razorbill.cl.cam.ac.uk Lines: 53 Status: O -- In article <9305201408.AA18558@enet-gw.pa.dec.com>, wallace@cookie.enet.dec.com ("Richard Wallace, CX02-1/7A, DTN:522-2792 20-May-1993 0806") writes: |> Dr. Botting of CSU, San Bernardio, CA, U.S.A writes: |> |> |If such a tool exists then it is either incomplete or it is in error since |> |it is possible to specify problems in Z that are not computable. |> |> Care to elaborate? I can see your point where you can have mappings of a |> specification to an incomplete mathematical system. That is to say the |> "Incompletedness" problem where one can specify that {x:Z * x :1/x} |> where 1/0 is not defined and thus by our incomplete mathematical system is |> "noncomputable." Such pitfalls can be avoided by a source code generation |> system if current compiler optimization technology is applied. Talk to anybody |> who has created an Ada compiler about range constraint violation checking during |> static semantic analysis and you'll lean that these issues can be forseen. |> |> Thus the tool may not be generating errors, but may be only able to do limited |> (read as "cheap or sloppy") static semantic analysis. |> |> Richard Wallace |> Senior Software Engineer |> Digital Equipment Corporation |> 301 Rockrimmon Blvd. South |> CXO2-1/7A |> Colorado Springs, CO 80919-2398 |> (719)548-2792 |> |> |> "The opinions expressed are my own, B.P. may not *quite* agree..." I think its more than that. I would expect that if you knew a little more about this than I that you could use Z to specify a funtion "halts" that took a natural number (the Godel number of some program) and some input (say another natural number) and returned true or false depending upon wether the program denoted by that Godel number terminates for that input. That is, I think you should be able to specify the halting problem in Z, but as we all know you can not find a general solution to the halting problem, therefore we know that there must be functions that you can specify in Z but that can not be automatically translated to code. Jim =============================================================================== Jim Grundy University of Cambridge | Phone: +44 223 334760 | This space has Computer Laboratory | Fax: +44 223 334678 | been intentionally New Museums Site | Telex: CAMSPLG 81240 | left blank for Pembroke Street | email: jg@cl.cam.ac.uk | formatting Cambridge CB2 3QG | | purposes. UNITED KINGDOM | | =============================================================================== From nic.csu.net!silicon.csci.csusb.edu!dick Mon May 24 11:23:57 1993 Relay-Version: VMS News - V6.1B5 17/9/92 VAX/VMS; site nic.csu.net Path: nic.csu.net!silicon.csci.csusb.edu!dick Newsgroups: comp.specification.z Subject: Re: Z spec generating C code Message-ID: <1993May19.170933.5344@nic.csu.net> From: dick@silicon.csci.csusb.edu (Dr. Richard Botting) Date: 19 May 93 17:09:31 PDT Nntp-Posting-Host: silicon.csci.csusb.edu X-Newsreader: Tin 1.1 PL4 Lines: 9 Status: O If such a tool exists then it is either incomplete or it is in error since it is possible to specify problems in Z that are not computable. -- dick::="Dr. Richard John Botting". csusb::="California State University, San Bernardino". dick@silicon.csci.csusb.edu=rbotting@wiley.csusb.edu. Cookie::="If god had wanted me to use UNIX I wouldn't have 10 thumbs.". Disclaimer::="I don't like Z or C.". From nic.csu.net!csus.edu!wupost!crcnis1.unl.edu!moe.ksu.ksu.edu!zaphod.mps.ohio-state.edu! Mon May 24 11:23:58 1993 Relay-Version: VMS News - V6.1B5 17/9/92 VAX/VMS V5.5-2; site nic.csu.net Path: nic.csu.net!csus.edu!wupost!crcnis1.unl.edu!moe.ksu.ksu.edu!zaphod.mps.ohio-state.edu! math.ohio-state.edu!magnus.acs.ohio-state.edu!usenet.ins.cwru.edu!gatech!swrinde!cs.utexas.edu!uunet!pipex!uknet!comlab.ox.ac.uk!ptb Newsgroups: comp.specification.z Subject: Re: Z spec generating C code Message-ID: <1993May21.134559.10016@topaz.comlab.ox.ac.uk> From: ptb@prg.ox.ac.uk (Peter Breuer) Date: Fri, 21 May 1993 13:45:59 GMT Reply-To: Peter.Breuer@prg.oxford.ac.uk (Peter Breuer) Sender: ptb@comlab.ox.ac.uk (Peter Breuer) References: <9305201408.AA18558@enet-gw.pa.dec.com> <1993May20.145012.16431@infodev.cam.ac.uk> Organization: Oxford University Computing Laboratory, UK Originator: ptb@topaz.comlab Lines: 45 Status: O In article <1993May20.145012.16431@infodev.cam.ac.uk> jg@cl.cam.ac.uk writes: >-- > >In article <9305201408.AA18558@enet-gw.pa.dec.com>, wallace@cookie.enet.dec.com ("Richard Wallace, CX02-1/7A, DTN:522-2792 20-May-1993 0806") writes: >|> Dr. Botting of CSU, San Bernardio, CA, U.S.A writes: >|> >|> |If such a tool exists then it is either incomplete or it is in error since >|> |it is possible to specify problems in Z that are not computable. >|> >|> Care to elaborate? I can see your point where you can have mappings of a >|> specification to an incomplete mathematical system. That is to say the >|> "Incompletedness" problem where one can specify that {x:Z * x :1/x} >|> where 1/0 is not defined and thus by our incomplete mathematical system is >|> "noncomputable." Such pitfalls can be avoided by a source code generation >|> system if current compiler optimization technology is applied. Talk to anybody >|> who has created an Ada compiler about range constraint violation checking during >|> static semantic analysis and you'll lean that these issues can be forseen. >|> >|> Thus the tool may not be generating errors, but may be only able to do limited >|> (read as "cheap or sloppy") static semantic analysis. >|> >I think its more than that. I would expect that if you knew a little more >about this than I that you could use Z to specify a funtion "halts" that >took a natural number (the Godel number of some program) and some input ... Precisely. But rather simpler things are practically speaking impossible to turn from specification into code. The intersection x = cap { s: P Z | 1 in s } is `known' to be the singleton { 1 } by anyone with the slightest bit of set theory to their name. That excludes compilers. Show me one compiler that can turn such a specification into anything other than a calculation that fruitlessly checks all integers to see if they're included in all subsets which include 1. It also excludes people with a _lot_ of knowledge, because they're bound to ask uncomfortable questions. Like what happens if the intersection is restricted to the infinite subsets, and what happens to the old boot that the almighty put in as the last element of every infinite set. - Peter From nic.csu.net!csus.edu!wupost!uunet!pipex!uknet!comlab.ox.ac.uk!ptb Mon May 24 11:23:58 1993 Relay-Version: VMS News - V6.1B5 17/9/92 VAX/VMS V5.5-2; site nic.csu.net Path: nic.csu.net!csus.edu!wupost!uunet!pipex!uknet!comlab.ox.ac.uk!ptb Newsgroups: comp.specification.z Subject: Re: Z spec generating C code Message-ID: <1993May18.104012.570@topaz.comlab.ox.ac.uk> From: ptb@prg.ox.ac.uk (Peter Breuer) Date: Tue, 18 May 1993 10:40:12 GMT Reply-To: Peter.Breuer@prg.oxford.ac.uk (Peter Breuer) Sender: ptb@comlab.ox.ac.uk (Peter Breuer) References: Organization: Oxford University Computing Laboratory, UK Originator: ptb@topaz.comlab Lines: 42 Status: O In article yadalle@amisk.cs.ualberta.ca writes: > Is there a programme that generates C code form a Z spec? >-- >Dave Shariff Yadallee (B. Sc.(Econ/Math) (U of Alberta 1990) ) I will look forward to the answer to this one (I think we should all be told ...)! I doubt it, in the sense I suppose you mean. There is a refinement method being worked on at Oxford that may help you produce working source code from a specification, using the B tool as part of the technique. But I'm out of contact with sort of thing, and the authors may well reply themselves soon (so I won't misquote them ahead of time). It surely doesn't produce C - at least I hope not; I don't have a hat to eat. There have been numerous efforts in the past to produce logic programming code directly from Z specifications, and functional programming code from a functional subset. Neither may be what you want, but I'll be glad to send you the references I have, if you give the nod. Here's a sample: @inproceedings{Z:Dick90, author = {A.J.J. Dick and P.J. Krause and J. Cozens}, title = {Computer Aided Transformation of {Z} into {Prolog}}, booktitle = {{Z} User Workshop, {Oxford} 1989}, editor = {J.E. Nicholls}, publisher = {Springer-Verlag}, series = {Workshops in Computing}, location = {Rewley House, Oxford, UK, 15 December 1989}, pages = {71-85}, year = {1990} } Any of the extant tools could be modified to produce C, at the cost of a heavy investment of time and effort round the back end. But I don't know precisely which tools are still being maintained. We'd better both go away and read the FAQ. -- Peter From nic.csu.net!silicon.csci.csusb.edu!dick Mon May 24 11:23:59 1993 Relay-Version: VMS News - V6.1B5 17/9/92 VAX/VMS; site nic.csu.net Path: nic.csu.net!silicon.csci.csusb.edu!dick Newsgroups: comp.specification.z Subject: Re: Z spec generating C code Message-ID: <1993May21.113140.5361@nic.csu.net> From: dick@silicon.csci.csusb.edu.csci.csusb.edu (Dr. Richard Botting) Date: 21 May 93 11:31:39 PDT References: <1993May20.145012.16431@infodev.cam.ac.uk> Nntp-Posting-Host: silicon.csci.csusb.edu X-Newsreader: TIN [version 1.1 PL9] Lines: 37 Status: O Jim Grundy (jg@cl.cam.ac.uk) wrote: : -- : In article <9305201408.AA18558@enet-gw.pa.dec.com>, wallace@cookie.enet.dec.com ("Richard Wallace, CX02-1/7A, DTN:522-2792 20-May-1993 0806") writes: : |> Dr. Botting of CSU, San Bernardio, CA, U.S.A writes: : |> : |> |If such a tool exists then it is either incomplete or it is in error since : |> |it is possible to specify problems in Z that are not computable. : |> : |> Care to elaborate? I can see your point where you can have mappings of a [...] : I think its more than that. I would expect that if you knew a little more : about this than I that you could use Z to specify a funtion "halts" that : took a natural number (the Godel number of some program) and some input : (say another natural number) and returned true or false depending upon wether : the program denoted by that Godel number terminates for that input. : That is, I think you should be able to specify the halting problem in Z, : but as we all know you can not find a general solution to the halting problem, : therefore we know that there must be functions that you can specify in Z but : that can not be automatically translated to code. : Jim Jim has hit the nail on the head - there exist problem statements that can not be solved by an effective procedure/algorithm/computer with infinite storage. Perhaps the 30 year search for "Automatic Programming" under various names is evidence that the problem of programming is one of these problems. If so then there is a place for humans in the software process between specification and coding. Something I think to be desirable. Disclaimer: One of Clarke's Laws states that when an aging scientist says that something is impossible, then he/she is usually wrong. From nic.csu.net!csus.edu!wupost!howland.reston.ans.net!usc!sol.ctr.columbia.edu!destroyer!cs.ubc.ca!unixg.ubc.ca!kakwa.ucs.ualberta.ca!yadalle Mon May 24 11:23:59 1993 Relay-Version: VMS News - V6.1B5 17/9/92 VAX/VMS V5.5-2; site nic.csu.net Path: nic.csu.net!csus.edu!wupost!howland.reston.ans.net!usc!sol.ctr.columbia.edu!destroyer!cs.ubc.ca!unixg.ubc.ca!kakwa.ucs.ualberta.ca!yadalle Newsgroups: comp.specification.z Subject: Z spec generating C code Message-ID: From: yadalle@cs.UAlberta.CA (Yadallee Dave S) Date: Mon, 17 May 1993 21:52:23 GMT Reply-To: yadalle@amisk.cs.ualberta.ca Sender: news@kakwa.ucs.ualberta.ca Organization: University Of Alberta, Edmonton Canada Nntp-Posting-Host: cab103.cs.ualberta.ca Lines: 6 Status: O Is there a programme that generates C code form a Z spec? -- Dave Shariff Yadallee (B. Sc.(Econ/Math) (U of Alberta 1990) ) ( yadalle@amisk.cs.ualberta.ca) God Save the Queen, God Bless us All!Remember! Jesus saves lives from eternal damnation! Nova Scotia, install John Savage, on May 25th VOTE LIBERAL!