schoett@informatik.tu-muenchen.dbp.de (Oliver Schoett) (10/17/90)
In article <1990Oct12.172820.4771@cbnewsm.att.com> lfd@cbnewsm.att.com (leland.f.derbenwick) writes: > I don't know any easy answers to these problems; I now tend to see > executable specifications as more likely part of the problem than of the > solution. The following paper makes a number of points against executability of specification languages: @Article( HJ_89, Author= "I. J. Hayes and C. B. Jones", Title= "Specifications are not (necessarily) executable", Journal= "Software Engineering Journal", Year= "1989", Month= nov, Pages= "330--338") Oliver Schoett Institut f. Informatik, Technische Univ. M"unchen Postfach 20 24 20, 8000 M"unchen 2, Germany schoett@informatik.tu-muenchen.dbp.de +49 89 2105 2390 schoett%informatik.....de@ {relay.cs.net, unido.uucp, dfngate.bitnet}
brendan@batserver.cs.uq.oz.au (Brendan Mahony) (10/18/90)
schoett@informatik.tu-muenchen.dbp.de (Oliver Schoett) writes: >The following paper makes a number of points against executability of >specification languages: The primary reason from avoiding executable specification languages is that it is sometimes necessary to discuss problems outside of the realm of computable functions. An important example of this is specifying the termination of a program. -- 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.
yodaiken@chelm.cs.umass.edu (victor yodaiken) (10/19/90)
In article <5289@uqcspe.cs.uq.oz.au> brendan@batserver.cs.uq.oz.au writes: >schoett@informatik.tu-muenchen.dbp.de (Oliver Schoett) writes: > >>The following paper makes a number of points against executability of >>specification languages: > >The primary reason from avoiding executable specification languages is >that it is sometimes necessary to discuss problems outside of the realm >of computable functions. An important example of this is specifying the >termination of a program. > Why would you need to be able to specify divergent programs? What possible computational interpretation would such a specification correspond to? >-- >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.
brendan@batserver.cs.uq.oz.au (Brendan Mahony) (10/21/90)
yodaiken@chelm.cs.umass.edu (victor yodaiken) writes: >Why would you need to be able to specify divergent programs? >What possible computational interpretation would such a specification >correspond to? No you want to be able to specify that it does not diverge! You can't do this in any executable notation. -- 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.
yodaiken@chelm.cs.umass.edu (victor yodaiken) (10/22/90)
In article <5321@uqcspe.cs.uq.oz.au> brendan@batserver.cs.uq.oz.au writes: >yodaiken@chelm.cs.umass.edu (victor yodaiken) writes: > >>Why would you need to be able to specify divergent programs? >>What possible computational interpretation would such a specification >>correspond to? > >No you want to be able to specify that it does not diverge! You can't do >this in any executable notation. > In a well defined executable notation, you should only be able to specify systems that will not diverge. That is, construction of a specification should itself constitute a proof that the specified system is non divergent.
chou@oahu.cs.ucla.edu (Ching-Tsun Chou) (10/23/90)
In article <21617@dime.cs.umass.edu> yodaiken@chelm.cs.umass.edu (victor yodaiken) writes: [.....] >In a well defined executable notation, you should only be able to specify >systems that will not diverge. That is, construction of a specification >should itself constitute a proof that the specified system is non >divergent. Think about this: Can you design a programming language in which ALL and NOTHING BUT total (in the sense of being convergent for all inputs) recursive functions can be described?
turpin@cs.utexas.edu (Russell Turpin) (10/23/90)
----- In article <40496@shemp.CS.UCLA.EDU>, chou@oahu.cs.ucla.edu (Ching-Tsun Chou) writes: > Think about this: > > Can you design a programming language in which ALL and NOTHING BUT total > (in the sense of being convergent for all inputs) recursive functions > can be described? Not in any reasonable fashion. If I had such a language, the first program I would write would be a general Turing machine simulator, ie, a program with a list of parameters p1, p2, ... that describe the TM's transition states and its input tape. Of course, for those parameters describing Turing machines that do not halt, the program would be rejected. Wow! A compiler that solves the halting problem. The alternative is a programming language that does not permit one to write a Turing machine simulator. This is a pretty poor excuse for a language. (In some unimportant senses, your request is possible. For example, an ordering can be described for the set of total recursive functions, and one can then "specify" them with the natural numbers: the program "0" corresponds to the first such function, "1" to the second, etc. Of course, one cannot *execute* such programs.) Russell
tgg@otter.hpl.hp.com (Tom Gardner) (10/23/90)
A couple of points: - just because an executable specification language/system cannot cover all points does not make it useless - there are many problems for which an executable specification would greatly improve the quality of the resulting system - even if you have a rigorous complete and self-consistent version of a system (and you can add any other hooray words that you like to this list), how would you know that (a) the _specification_ is correct (b) the specification accurately reflects what will occur in the real world (c) the specification is what the user/customer wants - every program that I have ever written or will ever write is an executable specification What I want is any tool which will improve the quality of the end system: I am not too concerned if it can't tackle _every_ problem (I'm not going to use a shovel to dig theChannel Tunnel, nor am I going to use a tunnel-boring machine to dig my vegetable garden). Yes, I do realise that I am subtly misunderstanding/misinterpreting some of the concepts behind "executable specifications". I do this so that the baby isn't thrown out with the bathwater.
yodaiken@chelm.cs.umass.edu (victor yodaiken) (10/23/90)
In article <40496@shemp.CS.UCLA.EDU> chou@oahu.cs.ucla.edu (Ching-Tsun Chou) writes: >In article <21617@dime.cs.umass.edu> yodaiken@chelm.cs.umass.edu (victor yodaiken) writes: > >[.....] > >>In a well defined executable notation, you should only be able to specify >>systems that will not diverge. That is, construction of a specification >>should itself constitute a proof that the specified system is non >>divergent. > > >Think about this: > >Can you design a programming language in which ALL and NOTHING BUT total >(in the sense of being convergent for all inputs) recursive functions >can be described? What is the purpose of a programming language? If it is to describe "effective computations" in the mathematical sense, then you are correct. If, on the other hand, the purpose of a programing language is to describe computations that are feasable on digital computers, we have some immediate constraints. There is an article by Parikh (Journal of Symbolic Logic 1977?) which suggests that an arithmetic restricted to exponentially computable functions might be sufficient. An earlier paper, by Cobham, argues that the polynomially computable functions are sufficient. Also, you might be interested in Predicative Arithmetic by Nelson. Nelson shows that it is possible to derive a large chunk of number theory from an axiomatization of arithmetic that is entirely devoid of impredicative methods. Turing machines are models of *effective computation*, not feasable computation.
brendan@batserver.cs.uq.oz.au (Brendan Mahony) (10/24/90)
tgg@otter.hpl.hp.com (Tom Gardner) writes: >A couple of points: > - just because an executable specification language/system cannot > cover all points does not make it useless > - there are many problems for which an executable specification > would greatly improve the quality of the resulting system Really you are arguing for higher level programming languages. Few will complain about that. If it is a specification language it should at least be able to specificy that the required program is to terminate. This is an awefully common requirement. > - even if you have a rigorous complete and self-consistent version > of a system (and you can add any other hooray words that you like > to this list), how would you know that > (a) the _specification_ is correct I get this a lot. I still have not met anyone who could define what it means. Correct with respect to what. Correctness is a property of answers (implementations) not questions (specifications). You should ask if the specification is appropriate. > (b) the specification accurately reflects what will occur > in the real world This is a question of the accuracy of the world model being used, which is a physics/engineering problem. In any case there can be no real world model in an executable language, it just ain't recursively enumerable. > (c) the specification is what the user/customer wants This is I think what you really meant with (a). > - every program that I have ever written or will ever write is an > executable specification Exactly. An executable specification language is by definition a programming language. -- 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.
chou@oahu.cs.ucla.edu (Ching-Tsun Chou) (10/24/90)
In article <21665@dime.cs.umass.edu> yodaiken@chelm.cs.umass.edu (victor yodaiken) writes: [.....] >What is the purpose of a programming language? If it is to describe >"effective computations" in the mathematical sense, then you are correct. >If, on the other hand, the purpose of a programing language is to describe >computations that are feasable on digital computers, we have some immediate >constraints. There is an article by Parikh (Journal of Symbolic Logic 1977?) >which suggests that an arithmetic restricted to exponentially computable >functions might be sufficient. An earlier paper, by Cobham, argues that >the polynomially computable functions are sufficient. [.....] I never read those papers, so I can't comment on them. But somehow I suspect that, if your programming language allows you to write only (say) polynomial-time computable functions, there got to be some simple functions which cannot be written in a "natural" way, because your program would constitute a proof of the polynomial-time computability of the function being programmed, and we all know that such proofs are not always easy. While such proofs are certainly desirable, you may not want them to be part of your specification, which presumably should convey what is to be computed, not how the computation is to be done. In order to be able to separate different concerns, I'm afraid the possibility of specifying non-polynomial computability, even non-recursiveness, in your language is something that has to be tolerated. Incidentally, I wonder how you specify Traveling Salesman Problem if you can only write polynomial-time computable functions. - Ching Tsun
rim@csadfa.cs.adfa.oz.au (Bob McKay) (10/26/90)
From article <5391@uqcspe.cs.uq.oz.au#, by brendan@batserver.cs.uq.oz.au (Brendan Mahony):
# tgg@otter.hpl.hp.com (Tom Gardner) writes:
#> - even if you have a rigorous complete and self-consistent version
#> of a system (and you can add any other hooray words that you like
#> to this list), how would you know that
#> (a) the _specification_ is correct
# I get this a lot. I still have not met anyone who could define what it
# means. Correct with respect to what. Correctness is a property of
# answers (implementations) not questions (specifications). You should ask
# if the specification is appropriate.
There are some correctness conditions that a specification clearly ought to
satisfy. Eg specifications that are either valid or unsatisfiable formulae of
whatever formalism is used are pretty useless. But I would imagine that in any
formalism that was powerful enough for useful specifications these would be
undecidable properties,
Cheers
Bob McKay Phone: +61 6 268 8169 fax: +61 6 268 8581
Dept. Computer Science ACSNET,CSNET: rim@csadfa.cs.adfa.oz
Aust. Defence Force Academy UUCP: ...!uunet!munnari!csadfa.cs.adfa.oz!rim
Canberra ACT 2600 AUSTRALIA ARPA: rim%csadfa.cs.adfa.oz@uunet.uu.net