Path: utzoo!attcan!uunet!cs.utexas.edu!tut.cis.ohio-state.edu!rutgers!mcnc!duke!romeo!crm
From: crm@romeo.cs.duke.edu (Charlie Martin)
Newsgroups: comp.software-eng
Subject: Re: Re: "Program Proving"
Message-ID: <18294@duke.cs.duke.edu>
Date: 19 Mar 90 13:25:15 GMT
References: <52044@microsoft.UUCP> <2480007@hpcuhc.HP.COM>
Sender: news@duke.cs.duke.edu
Reply-To: crm@romeo.UUCP (Charlie Martin)
Organization: Duke University CS Dept.; Durham, NC
Lines: 45

In article <2480007@hpcuhc.HP.COM> runyan@hpcuhc.HP.COM (Mark Runyan) writes:
>Your telling me that formal proofs are *only* useful on new development?
>Considering how much old code is out there, I find this slightly 
>frightening.

Gee, don't be frightened, Mark.  It's no more of a boogeyman than it was
before.

Gee, on second thought, maybe I'll be frightened with you.

>
>Still, anything that can be used to improve new code is a plus.  But at
>the moment, I'm trying to fight fires in old code where total replacement
>is *not* considered an alternative.

The very first experience I had with program proof in real code was in
Germany in 1981.  I'd just read _The Science of Programming_.  The
system I was working on (I was the warranty) had a module that had just
been unending trouble.  It controlled a big n x n switch matrix, and the
matrix had a tendency not to switch correctly, but intermittently.

The hardware guys swore it was software problems; after some time, in
desperation I rewrote and proved the single routine that generated the
message to which the switch responded.  I reinstalled that module and
--- the switch still didn't work.  Since I had not only proven the
routine but tested the hell out of it (pace Fetzer) I was reasonably
confident that THIS module was generating the correct controls.  With
this basis, I was confident enough to tell the hardware guys that it was
absolutely not the software, could we put a logic analyzer on the
control lines.  When we did, the control signals were as specified.  It
was the box after all.  (Turned out the switch settings were set up
through an eprom, which had been xrayed coming through the export
process.)

The point of this, yet another war story, is that I got good results
during maintenance by removing one routine of about 75 lines which was
apparently real trouble and then reimplementing it with proof.  Since
many systems exhibit the 80/20 fault behavior (80 percent of the faults
lie in 20 percent of the modules) I suspect that hand-proof can be used
during maintenance to fix the buggiest modules first and get a LOT of
improvement in reliability.  The same could be said of machine-checked
proof, but machine-checked proof is higher cost.


Charlie Martin (crm@cs.duke.edu,mcnc!duke!crm)