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 Subject: Re: No Go To's Forever! Date: 2000/03/24 Message-ID: <8bg23k$skv$1@nnrp1.deja.com>#1/1 X-Deja-AN: 601785019 References: <8bdbof$t19$1@nnrp1.deja.com> <8berdq$j2p$1@nnrp1.deja.com> X-Http-Proxy: 1.0 x21.deja.com:80 (Squid/1.1.22) for client 205.232.38.14 Organization: Deja.com - Before you buy. X-Article-Creation-Date: Fri Mar 24 15:37:26 2000 GMT X-MyDeja-Info: XMYDJUIDrobert_dewar Newsgroups: comp.lang.ada X-Http-User-Agent: Mozilla/4.61 [en] (OS/2; I) Date: 2000-03-24T00:00:00+00:00 List-Id: In article <8berdq$j2p$1@nnrp1.deja.com>, 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. To expand on this a bit. There are two loops here. Both are trivially tail recursive. The problem is of course proving *total* correctness in this algorithm, partial correctness is immediately obvious. If you separate the two loops clearly, you find that the proof conditions are very nicely separated. You have of course to introduce the auxiliary variable that shows how sorted the set of data is. You then concentrate on showing that the inner loop increments this auxiliary variable, and that is easy to show in isolation, i.e. by analyzing the inner loop separately. Now once this is shown a simple monotonicity argument applied to the outer loop proves correctness. I continue to be sure that the version in which the two loops are explicit is far clearer to understand and to analyze. It is very interesting that usually we object to gotos because they obscure the control structure, and that here the desparate attempt to get rid of the goto actually ends up *helping* to obscure the control structure. I wonder why it is that people are so allergic to gotos. Oddly this kind of furious allergy seems much more common in the US. Perhaps it is the conviction of the more recently converted. Those who grew up on Algol tend to have an easier time of maintaining a balanced view point :-) Sent via Deja.com http://www.deja.com/ Before you buy.