NetNews Usenet Archive 1992 #20/NN_1992_20.iso/spool/comp/lang/cplus/13338

Internet Message Format | 1992-09-08 | 4.0 KB

Path: sparky!uunet!usc!cs.utexas.edu!devnull!rgp
From: [e-mail] (Ramon Pantin)
Newsgroups: comp.lang.c++
Subject: Re: GOTO, was: Tiny proposal for na
Message-ID: <[e-mail]>
Date: 5 Sep 92 17:31:35 GMT
References: <[e-mail]> <rmartin.715102882@thor> <[e-mail]>
Sender: [e-mail]
Organization: Tandem Computers, Micro-Products Division
Lines: 73

In article <[e-mail]> [e-mail] (James Kanze) writes:

>... The only "clear and convincing argument
>that the code is correct" must use logical proof of correctness concepts.
>These concepts, at least in the literature I've seen, *only* address the three
>basic forms of program flow: sequence, iteration and conditional.  In particular,
>to reason about program correctness, it is essential that each program block
>have one and only one point of entry and one and only one point of exit.

Mathematical reasoning tends to be "constructive" in nature.  If all non
structured programs (by the Structured Programming definition) can be
mechanically converted to structured programs, then it is not necesary
to investigate methods for proving non structured programs correct,
correctnes of non-structured programs can be proven by transforming them
into structured programs and then proving those correct.

The fact that the literature shows research in the areas of proving program
correctness doesn't preclude YOU from reasoning in any way you want about
your program's correctness.  BTW, the research that I've seen is directed
at mechanically proving things correct, not as thinking aids for programmers.

It seems that for some programmers (like me) it is harder to think about
correctness when we see pascaloid code with lots of state variables, lots
of places where they are tested and set, lots of indentation as the result
of not using breaks, continues or returns.  Some other programmers (like
you and Mr. Martin) prefer to reason about programs that simply avoid all
the non-SP contructs and replace them with state variables, duplicated
code and lots of indentation.

>...

>On the other hand, you *cannot* use break or continue, since these mimic a
>goto to somewhere you *do not* what to go to.  In the same way, how do you
>prove a function correct if it returns somewhere from the middle.

Very simple, mechanically transform it to SP and then mechanically prove
it correct.  How else?  Just run:
    $ nonsp2sp nonsp.c | prove - nonsp.specs
    $ echo $?
    0
    $

>Apparently most of the responses have been in favor of using break.  Do I
>conclude that most programmers just don't care about having correct programs?

Talking about logic, huh?  You can't conclude that!  (Can't use "leaps of
faith" in logic constructions).

There is a big difference between "having correct programs" and being
able to (or even wanting to) prove those programs correct!
Your statement indicates that programs that use "break" cannot be correct.
Or to put it your way, the programmers that use break cannot have correct
programs.

A program can be correct even if nobody can prove it correct.  The truth
value of a logical proposition doesn't change if individuals that read it
can't determine its truth value (i.e. if they can't prove it or show a
counter example).  The world never stopped being quasi-spherical even if
nobody could prove it, observe it, or believe it.

It is also important to note that most programmers are interested in
writting correct programs than being able to prove them correct.

When was the last time that YOU proved one of your "real world" programs
(at least 10000+ lines) correct?  How long did it take you?  Assuming that
you have ever done this, how did you felt when, after having proving it
correct, you found your first bug?  How did you prove that the prove was
correct (an so on) ?  How did you maintain the prove when you had to
maintain the program when a set of features was added?

Think and program as it better fits your brain.

Ramon Pantin