[comp.software-eng] Proofs

pat@megatest.UUCP (Patrick Powers) (01/12/91)

Harlan Mills has made studies that show that functional verification,
as opposed to Hoare's axiomatic verification, is helpful in producing
reliable software.  I've tried these techniques informally and found
that quite helpful in producing a large system.  There was a cover 
article about them in IEEE Software in about 1987 or 86.
-- 
--

crm@duke.cs.duke.edu (Charlie Martin) (01/14/91)

In article <1991Jan11.175952.10978@pdn.paradyne.com> locke@nike.paradyne.com (Richard Locke) writes:
>[not redirection from discussion in comp.object]
>
>Capers Jones makes the interesting statement that there isn't any
>empirical evidence that correctness proofs are an effective defect
>removal or defect prevention strategy (in the context of "real"
>product development efforts).
>
>Does anyone have evidence to dispute this?
>

Yes -- in fact, all the empirical evidence of which I am aware directly
contradicts this.  See, e.g. the papers on the Cleanroom methods, in
which Harlan Mills documents about an order of magnitude improvement in
defect rates at a 30 percent GAIN in productivity.  My own experience
suggests that somewhat different methods give perhaps 80 times
improvement in defect rates.

I'd like Mr Jones to quote the studies that didn't show an improvement.

-- 
Charlie Martin (...!mcnc!duke!crm, crm@summanulla.mc.duke.edu)
O: NBSR/One University Place/Suite 250/Durham, NC  27707/919-490-1966
H: 13 Gorham Place/Durham, NC 27705/919-383-2256

jimad@microsoft.UUCP (Jim ADCOCK) (01/16/91)

In article <1991Jan11.175952.10978@pdn.paradyne.com| locke@nike.paradyne.com (Richard Locke) writes:
|[not redirection from discussion in comp.object]
|
|Capers Jones makes the interesting statement that there isn't any
|empirical evidence that correctness proofs are an effective defect
|removal or defect prevention strategy (in the context of "real"
|product development efforts).
|
|Does anyone have evidence to dispute this?

Not disputing this -- but another data point:  A while back I asked on
notes for any "non-trivial" program examples from the "proving" camp
that I could compile and execute on a PC [since this is my development
environment], for my own edification, and I volunteered to report back to
the net what I found.  ["Non-trivial" was to be defined by the program-
submitter.]  I received no offers.

kambic@iccgcc.decnet.ab.com (01/16/91)

In article <14849@megatest.UUCP>, pat@megatest.UUCP (Patrick Powers) writes:
> Harlan Mills has made studies that show that functional verification,
> as opposed to Hoare's axiomatic verification, is helpful in producing
> reliable software.  I've tried these techniques informally and found
> that quite helpful in producing a large system.  There was a cover 
> article about them in IEEE Software in about 1987 or 86.
> -- 
> --
In addition, there was a recent bit of work done at Ames Research Center (NASA) 
that examined the use of a cleanroom technique in developing software.  I am
currently beating my head against my file cabinet because I loaned the file to
someone else.  The basis of the study is the use of paper verification
techniques in sw development.  The claim is great success for the series of
projects studied (better, faster, cheaper).  It was done in conjunction with
the U of Maryland.  I believe that one of the lead authors, if not the lead, is
Dr. Victor Basili at UM.  You could probably call NASA or UM to get a copy of
the paper.  I cannot remember where it was published.  Talk about a need for
duplicate files!

GXKambic