Path: utzoo!attcan!uunet!wuarchive!zaphod.mps.ohio-state.edu!rpi!bu.edu!husc6!m2c!umvlsi!dime!yodaiken
From: yodaiken@chelm.cs.umass.edu (victor yodaiken)
Newsgroups: comp.specification
Subject: Re: Against executable specifications (Re: specifying OBJ in itself)
Message-ID: <21617@dime.cs.umass.edu>
Date: 22 Oct 90 12:30:50 GMT
References: <6470@vanuata.cs.glasgow.ac.uk> <4955@tuminfo1.lan.informatik.tu-muenchen.dbp.de> <5289@uqcspe.cs.uq.oz.au> <21500@dime.cs.umass.edu> <5321@uqcspe.cs.uq.oz.au>
Sender: news@dime.cs.umass.edu
Reply-To: yodaiken@chelm.cs.umass.edu (victor yodaiken)
Organization: University of Massachusetts, Amherst
Lines: 15

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.