Re: No Go To's Forever!

[Robert Dewar <robert_dewar@my-deja.com>]

In article <8berdq$j2p$1@nnrp1.deja.com>,
  Robert Dewar <robert_dewar@my-deja.com> 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.