From: koen@blade.stack.urc.tue.nl (Koen Holtman)
Newsgroups: alt.folklore.computers
Subject: Re: Branching in HLL vs. Assembler (was Re: The need for an assembler)
Date: 28 Aug 92 14:02:01 GMT

dsiebert@icaen.uiowa.edu (Doug Siebert) writes:

>The reason people are taught that "all GOTOs are bad" in schools doesn't have
>anything to do with the fact the CPU can only do GOTOs, or that a structured
>statement like for or while compiles into code using GOTOs.  The reason is an
>outgrowth of the idea of mathematically "proving" programs correct.  Any code
>written with the traditional "structured" constructs can be mathematically
>proven correct, but if there is a GOTO in that code, forget it!

Nope!  Programs containing GOTO's can be proven correct just like any
other programs.  In fact, one of the first program proving systems 
(~1968, I believe) called "annotated flow charts" (or is that flaw
charts?) proved programs on flow charts (which are equivalent to a
language containig goto's) by using "cut points".

Most program proving systems don't cover the GOTO because:
- A program containing only "structured" constructs has a simple control
  flow. If the control flow is simple, proofs of termination can be
  short and easy. 
  A few GOTO statements, used in an "unstructured" way, tend to introduce
  loads of (potential) loops in the program, each of which has to be
  checked for termination. 
  A proof system including the GOTO has to define all potential loops in
  a spaghetti program, which makes it much more complicated than a
  "structured" proof system.
- A program without GOTO's can be devided into smaller parts,
  which can be proved independently.  You can't prove a program fragment
  containing a label indepentently, because GOTO's in the other parts
  might jump to it.
- You can live without the GOTO
- Most pioneers of program proving didn't like the GOTO anyway.

In fact, Dijkstra introduced what he called the "law of the excluded
miracle" (For no statement S  { P } S { False } holds), which all
statement definitions in a proof system should have to satisfy.
But there is a statement whose definition violates this law. It
is (surprise!) the GOTO statement. How's that for a hidden agenda.

>In reality, most of us aren't concerned with proving code correct.

I am.... It is a truly fascinating subject. But then again, I'm a student,
and get paid whether I write code or not.

[....]
>  Currently it is totally
>impractical to prove any but the tiniest programs correct, but it is possible
>that at some point a combination of new language designs and automation will
>make it feasible for reasonable-sized programs.

Well no. It depends on what you want.  Do you want a proof of a large
program so that you can be absolutely sure that it contains no bugs?
Forget it.  Proofs can be wrong.  People can make mistakes.  And as for
completely automated program provers, if one ever succeeds in building
one, we can't trust them any more than other programs.

It is quite possible to proof reasonable-sized programs (I have done
so). Such proofs are not a certification that the program actually will
work, they are used as the formal counterpart of our intuitive grip on the
subject.
The more you know about the program you are making, the greater
the chance that it will work. The proof generally ignores the trivial
parts of the program. As programs consist for a large part out of
trivialities, this kind of program proving doesn't take so mutch
time that it is totally unfeasible.  (Though it depends on your notion
of what is trivial, and how good you are with formal systems)

>However, I'm sure that purists like Mr. Lasner will still claim assembly is
>the best language and that writing provably correct programs in assembly is
>possible if you work hard enough at it :-)

Every program can be proven correct, provided that it doesn't contain
bugs :-)


>| Doug Siebert                             | "I don't have to take this abuse |

Koen.
_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _
Koen Holtman                  TUE computing science     "Dat zieje wel"
koen@blade.stack.urc.tue.nl    (Ax:*p)==(*p&p!=&x)         --Multatuli
Newsgroups: alt.folklore.computers