From: rh@smds.com (Richard Harter)
Newsgroups: alt.folklore.computers
Subject: Re: On the care and feeding of GOTOS
Date: 1 Sep 92 07:42:07 GMT
Reply-To: rh@ishmael.UUCP (Richard Harter)
Organization: Software Maintenance & Development Systems, Inc.


I, Richard Harter, wrote:

Or at least you can interpret them that way.  As Knuth observed in one
of his essays, proof of correctness of goto/label programming is very
simple -- for each label there is an assertion that states what conditions
must be satisfied for a legitimate transfer to that label.  For each
goto there must be a proof that the preconditions for transferring to
the target label hold.

	--------

Koen Holtman responds with:

This method is only sufficient for proving _partial_ correctness, that
is `if the program halts, it will have produced the right result'

For proving _total_ correctness, the program halts and gives the
right result, you need more than that.

Let's see.. Take an integer variable PUX that does not apear in the
original program, and replace all GOTO X statements by 
PUX:=PUX-1;GOTO X. Now prove with Knuth's method that during the
execution of the new program, the value of PUX will never drop
below zero. Assume any initial value for PUX that you want, and no,
infinity does not count as an integer.

If your program contains any (ack! ugh!) _structured_ loop constructs,
also add a PUX:=PUX-1 to the end of each loop body. 

If you can prove that PUX will never drop below zero, then you know that
the program will end. Needless to say, proving this is slightly unsimple
in most cases.

	--------

It took me a bit to see what you were getting at -- at first sight it
seemed like you were wandering off into left field.  What you say is
right, but misleading.  Suppose I have a program P with labels L1...Ln
and assertions A1...An for each label.  To establish correctness, we
need to establish for each transfer, goto Li, that the precondition
Ai for label Li is satisfied.  As you observe, correctness does not
necessarily imply termination.  And, of course, proof of termination
is not precluded -- it all depends on the content of the assertions.

In my view, the problem with GOTO's is that they have been used for
the wrong thing.  The GOTO in circa 1960 programming was used as a
primitive flow control construct.  It was correctly observed that
it was too primitive, that essential information was lost.  However
when I look at what correctness proofs for GOTO/labels demand, I
immediately think of event driven programming and state machines
and the like.  That is the natural domain of the GOTO.  A label is
the start of an event-handler.  A GOTO signifies completion of
processing of one event and the raising of another.  Naturally one
can't call it a GOTO -- we must respect tribal superstitions, after
all.

So us let introduce the term, software event handler (really a
label, but don't tell anyone), and the the term raise-software-event
(really a GOTO, but don't tell anyone).  And then we can go happily
off, writing our software event driven programs.  No one will ever
know the difference -- the software gurus can herald the new
revolution and busily market seminars in software-event-driven
programming.  A new generation of CS academics can write papers
on avoiding deadlock in sofware-event-driven programs.  Software
compiler houses can sell compilers for SED (software-event-driven)
languages, and OOSED (object oriented software event driven) languages.
A great future in software innovation beckons us.

:-) ?
-- 
Richard Harter: SMDS Inc.  Net address: rh@smds.com Phone: 508-369-7398 
US Mail: SMDS Inc., PO Box 555, Concord MA 01742.    Fax: 508-369-8272
In the fields of Hell where the grass grows high
Are the graves of dreams allowed to die.