Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!zaphod.mps.ohio-state.edu!pacific.mps.ohio-state.edu!linac!att!ucbvax!dog.ee.lbl.gov!elf.ee.lbl.gov!torek
From: torek@elf.ee.lbl.gov (Chris Torek)
Newsgroups: comp.lang.misc
Subject: Re: Formal definitions (Re: ada-c++ productivity)
Message-ID: <12318@dog.ee.lbl.gov>
Date: 21 Apr 91 00:14:21 GMT
References: <1726@optima.cs.arizona.edu> <29344@dime.cs.umass.edu> <12297@dog.ee.lbl.gov> <11204@uwm.edu>
Reply-To: torek@elf.ee.lbl.gov (Chris Torek)
Organization: Lawrence Berkeley Laboratory, Berkeley
Lines: 82
X-Local-Date: Sat, 20 Apr 91 17:14:21 PDT

(First one small note: my NAND definition was wrong; it should have read
`0 if a=1 and b=1, 1 otherwise'.  I am surprised that, given the usual
usenet tendency to turn one error into `your entire argument is wrong',
no one has done this yet. :-) )

>In article <12297@dog.ee.lbl.gov> I wrote:
>>[Some] people advocate `proving programs correct' because they believe
>>that the activity really does lead to correct programs.  Others advocate
>>testing because they believe that testing leads to correct programs.
>>Both groups are partially right: the process of reasoning about programs
>>often turns up bugs, and the process of testing often turns up bugs.
>>Both methods are fallible, because they are done by people, and because
>>they make assumptions that are sometimes false.

In article <11204@uwm.edu> markh@csd4.csd.uwm.edu (Mark William Hopkins)
writes:
>After spending the better part of a week testing software that I have already
>proven correct to find bugs that were never in the software but actually a
>result of the test conditions not exactly matching running conditions, and
>having this happen on *three* consecutive occasions I have no sympathy for
>the testing point of view.

This happens to me as well: a routine that I have `reasoned' correct fails
a test, and it turns out that the test is wrong.

>If it's proven mathematically, it *will* work.

(To argue David Gudeman's side:)  *What* will work?

If your proof is correct, you have shown that your program P1 in
language L1 is mathematically equivalent to some other program P2 in
some other language L2.  There are no guarantees that the assumptions
made in the process (that compiler C1 for language P1 `works', that
program P2 has the desired effect in all circumstances, and so on) are
all correct.

>And if it doesn't, then it's provably the fault of the underlying
>hardware (or compiler or assembler).

Quite so: software does not exist in a vacuum (unless perhaps Objective
Reality does not exist: perhaps I myself do not exist except as a
concept in a vacuum---but never mind that).

Moreover, you may have made an error in your proof (mathematicians *do*
make errors [why, I remember back in 1802 when . . . :-) ]), or your
specification language and program L2 and P2 may not describe what was
really supposed to have been programmed (i.e., the specification may be
in error; perhaps it omits a detail that should have been included, or
maybe it is just entirely wrong).

>But the point is, after verification, responsibility for proper
>functioning is no longer the software writer's job.  That job is complete.

If you wish to partition the jobs, you can certainly make this
statement.  Nonetheless I, for one, would not want to be put under an
X-ray machine running software that was proven but never tested.
Whether the software writer's job is complete or not, *someone* should
test such a critical system as this one.  Indeed, there should be
redundant error checks all down the line: from the specifications
through the hardware and software all the way to the machine's
operator.

>Software is valid, even when it does not function normally due to faulty
>hardware or translators.

Yet software that is `valid' by this definition can still `do the wrong
thing', even when the hardware or translators work.  In addition, if
the hardware and translators are fallible (and they are!), critical
software should incorporate redundant error checks anyway.

Again, this draws perilously close to the argument over where the
`line between wasted effort and irresponsibility' is to be drawn.

Remember, I am not claiming that proving programs correct is
valueless.  I (and I think David Gudeman as well) only claim that
a correctness proof is not a `magic bullet', and that it should be
used, where appropriate, in conjunction with other `bug avoidance'
techniques.  `When' and `how much' proof and/or testing is adequate
is problem-dependent.
-- 
In-Real-Life: Chris Torek, Lawrence Berkeley Lab CSE/EE (+1 415 486 5427)
Berkeley, CA		Domain:	torek@ee.lbl.gov