Re: No Go To's Forever!

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

In article <38E1F6D5.8303903C@dowie-cs.demon.co.uk>,
  Martin Dowie <martin@dowie-cs.demon.co.uk> wrote:
> speaking of proving things...
>
> one of the reasons I had always been told for avoiding using

gotos, was
> that it makes a program unprovable. a) was this true; and if

so, b) is
> this still true?


Well it's an overstatement, obviously limited forms of gotos
are totally equivalent to simple control structures and thus
neither harder or easier to prove correct.

It is true that the denotational semantics of a general goto
is very tricky. If any of you can dig out ancient materials,
have a look at the source code of Ada/Ed. This was basically
an executable denotational semantics. At this level, an
if statement was coded something like:

    if evaluate (expression) = true then
        replace if with then part
    else
        replace if with else part
    end;

the coding for goto was really complex and horrible (and
interestingly REALLY inefficient :-)

So yes, general gotos can definitely make proof of correctness
more difficult.


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