From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: *
X-Spam-Status: No, score=1.3 required=5.0 tests=BAYES_00,INVALID_MSGID,
	MSGID_RANDY autolearn=no autolearn_force=no version=3.4.4
X-Google-Language: ENGLISH,ASCII-7-bit
X-Google-Thread: 103376,14f7200925acb579
X-Google-Attributes: gid103376,public
From: Robert Dewar <robert_dewar@my-deja.com>
Subject: Re: No Go To's Forever!
Date: 2000/04/17
Message-ID: <8df2ub$inj$1@nnrp1.deja.com>#1/1
X-Deja-AN: 612212756
References: 
 <Pine.SOL.4.21.0003212347450.15450-100000@fraggel81.mdstud.chalmers.se>
 <8bdbof$t19$1@nnrp1.deja.com> <tNwC4.964$q41.1034@news.pacbell.net>
 <8berdq$j2p$1@nnrp1.deja.com> <sfke9p2pivv17@corp.supernews.com>
X-Http-Proxy: 1.0 x32.deja.com:80 (Squid/1.1.22) for client 205.232.38.14
Organization: Deja.com - Before you buy.
X-Article-Creation-Date: Mon Apr 17 13:18:14 2000 GMT
X-MyDeja-Info: XMYDJUIDrobert_dewar
Newsgroups: comp.lang.ada
X-Http-User-Agent: Mozilla/4.61 [en] (OS/2; I)
Date: 2000-04-17T00:00:00+00:00
List-Id: <comp.lang.ada>

In article <sfke9p2pivv17@corp.supernews.com>,
  ka@exit109.com (Kenneth Almquist) wrote:
> Robert Dewar wrote:
> > But there really is a very fundamental point here. If you
> > want
> > to study it further, try generating the full denotational
> > semantics and in fact try generating the full proof
conditions.
> > That will make things clearer I think.

Interesting post, but I am afraid not quite I asked for,
the most important word in my above quote here is denotational.
You gave a proof in terms of operational semantics, and I
will repeat my claim that you will more easily see the
fundamental difference between the two algorithms if you
look at things at a higher level, which is where the
denotational semantics will lead you. Basically you want
to think in terms of what the parts of the program *mean*
instead of what they *do*, and that of course is the
fundamental distinction between denotational and operational
semantics.

True the distinction is not always clear. Indeed Ada/Ed was
in many respects an operational version of a denotational
semantic definition for Ada.

At an operational level, it is fairly easy to see that the
two forms are equivalent, as you show in your proof, but
it is much more difficult to see this equivalence at the
denotational semantic level.


Sent via Deja.com http://www.deja.com/
Before you buy.