Path: utzoo!attcan!uunet!munnari.oz.au!csc.anu.oz.au!csc3.anu.oz.au!ccadfa!rim@csadfa.cs.adfa.oz.au
From: rim@csadfa.cs.adfa.oz.au (Bob McKay)
Newsgroups: comp.specification
Subject: Re: Against executable specifications (Re: specifying OBJ in itself)
Message-ID: <1990@ccadfa.adfa.oz.au>
Date: 26 Oct 90 00:40:42 GMT
References: <5391@uqcspe.cs.uq.oz.au>
Sender: gco@ccadfa.adfa.oz.au
Lines: 21

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