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

Text File | 1992-09-09 | 6.0 KB | 131 lines

Newsgroups: comp.lang.c++
Path: sparky!uunet!haven.umd.edu!darwin.sura.net!Sirius.dfn.de!ira.uka.de!slsvaat!josef!kanze
From: [e-mail] (James Kanze)
Subject: Re: GOTO, was: Tiny proposal for na
In-Reply-To: [e-mail]'s message of 5 Sep 92 17:31:35 GMT
Message-ID: <[e-mail]>
Sender: [e-mail]
Organization: SEL
References: <[e-mail]> <rmartin.715102882@thor>
    <[e-mail]> <[e-mail]>
Date: 9 Sep 92 21:05:21
Lines: 117

In article <[e-mail]> [e-mail] (Ramon Pantin) writes:

> 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.

Apparently, I've been misunderstood here.  I was *not* talking about
mechanically proving programs correct, but using some sort of logical
reasoning as a thinking aid.

I imagine that, like me, most C++ programmers are involved in
developing real life projects.  We do not have the tools for
mechanical proof available, and if we did, we probably wouldn't have
the time to input the logical specifications necessary to use them.

Which, of course, does not mean that we shouldn't try to analyse our
programs logically.

> 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.

Interestingly, although it doesn't seem to work in artificially
contrived examples, I find that having to reason carefully about what
my code does tends to reduce the number of indentations, etc.
(Although it may increase the total number of functions.)  I'm not
saying that it's impossible to reason about unstructured code, just
that it's more difficult.  I find it more cost-efficient to structure
the code; any additional time necessary to write it is more than made
up for by the lesser amount of time used in analysis.  (And of course,
the time used in analysis is definitely made up for by the time saved
in error correction.)

> >...

> >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).

(I think I forgot a smiley.  The remark was meant to be partially
humorous.)

> 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.

No, my statement is that you cannot know that it is 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.

But then how do they know they are correct?

Most programmers I know do want to write correct programs.  And of
course, even with proof of correctness...  Proof of correctness is
just one more arm in the fight.  It's usually a pretty good arm *at
the lower levels*.  (It'll never prove that the customer will be
satisfied with the program, which is what I really want.  It will help
to reduce the price of the program, and also the number of errors in
the delivered program.  My customers tend to consider this a positive
aspect.)

> 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?

See the above comment.  Neither proof of correctness, nor any
structured programming technique, will prove that you've solved the
right problem.

I find OO programming and structured programming complementary.  The
OO stuff helps do the high level design stuff, but you still need the
structure and logical reasoning for the low level nitty-gritty, making
sure that each function does what you think it should.

In a well defined application, you can expect about one error per
10000 lines of code using informal proof of correctness (plus all of
the other means at your disposal).  You can do better, but unless the
system is particularly critical, it probably isn't cost efficient.

> Think and program as it better fits your brain.
--
James Kanze                         GABI Software, Sarl.
email: [e-mail]           8 rue du Faisan
                                    67000 Strasbourg
                                    France