Path: utzoo!utgpu!jarvis.csri.toronto.edu!cs.utexas.edu!usc!brutus.cs.uiuc.edu!ux1.cso.uiuc.edu!ux1.cso.uiuc.edu!m.cs.uiuc.edu!render
From: render@m.cs.uiuc.edu
Newsgroups: comp.object
Subject: Re: Reasons why you don't prove your pr
Message-ID: <77500026@m.cs.uiuc.edu>
Date: 18 Jan 90 01:38:23 GMT
References: <7578@hubcap.clemson.edu>
Lines: 22
Nf-ID: #R:hubcap.clemson.edu:7578:m.cs.uiuc.edu:77500026:000:1209
Nf-From: m.cs.uiuc.edu!render    Jan 17 14:01:00 1990


Written 12:15 pm  Jan 16, 1990 by jimad@microsoft.UUCP:
>Again: 'proving' that software is correct does nothing to improve the
>quality of that software.  Finding and removing bugs does improve the
>quality of software.  

Wrong. Finding and removing errors is testing.  And, as has oft been noted, 
testing can only determine the presence of errors, not their absence.  By 
proving software "correct" (actually proving that the software meets some 
formal specification), one attempts to show that there are no errors in 
the software (w.r.t the specification).  The process of proving a program
correct should either indicate that there are no errors or should indicate
that there are (and often what and where they are).  Thus, successful program 
proving methods should eliminate the need for testing.  In practice things 
are not so straightforward, because verification is tough to do for many kinds
of programs, and one still has to contend with erroneous specifications.

BTW, if anyone hasn't read the December CACM exchange between Dijkstra, Parnas
and the others, they should do so now.  Even though he sounds like a crank,
Dijkstra raises a lot of good points pertinent to this discussion. 

hal.