Path: utzoo!attcan!uunet!wuarchive!usc!elroy.jpl.nasa.gov!ucla-cs!oahu.cs.ucla.edu!chou
From: chou@oahu.cs.ucla.edu (Ching-Tsun Chou)
Newsgroups: comp.specification
Subject: Re: Against executable specifications (Re: specifying OBJ in itself)
Message-ID: <40496@shemp.CS.UCLA.EDU>
Date: 22 Oct 90 20:22:35 GMT
References: <21500@dime.cs.umass.edu> <5321@uqcspe.cs.uq.oz.au> <21617@dime.cs.umass.edu>
Sender: news@CS.UCLA.EDU
Organization: UCLA Computer Science Department
Lines: 15
Nntp-Posting-Host: oahu.cs.ucla.edu

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?