[comp.specification] Against executable specifications

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