Path: utzoo!utgpu!news-server.csri.toronto.edu!rutgers!sun-barr!olivea!samsung!munnari.oz.au!brolga!uqcspe!batserver.cs.uq.oz.au!brendan
From: brendan@batserver.cs.uq.oz.au (Brendan Mahony)
Newsgroups: comp.specification
Subject: Re: Against executable specifications (Re: specifying OBJ in itself)
Message-ID: <5391@uqcspe.cs.uq.oz.au>
Date: 24 Oct 90 06:59:46 GMT
References: <4955@tuminfo1.lan.informatik.tu-muenchen.dbp.de> <28190001@otter.hpl.hp.com>
Sender: news@uqcspe.cs.uq.oz.au
Reply-To: brendan@batserver.cs.uq.oz.au
Lines: 45

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.