Xref: utzoo comp.ai:5578 comp.edu:2924 comp.object:755
Path: utzoo!utgpu!jarvis.csri.toronto.edu!cs.utexas.edu!uwm.edu!csd4.csd.uwm.edu!markh
From: markh@csd4.csd.uwm.edu (Mark William Hopkins)
Newsgroups: comp.ai,comp.edu,comp.object
Subject: Re: Reasons why you don't prove your programs are correct
Message-ID: <1928@uwm.edu>
Date: 16 Jan 90 23:23:49 GMT
References: <16479@joshua.athertn.Atherton.COM> <1455@krafla.rhi.hi.is> <16665@joshua.athertn.Atherton.COM> <10289@microsoft.UUCP>
Sender: news@uwm.edu
Reply-To: markh@csd4.csd.uwm.edu (Mark William Hopkins)
Followup-To: comp.ai
Organization: University of Wisconsin-Milwaukee
Lines: 45

In article <10289@microsoft.UUCP> jimad@microsoft.UUCP (JAMES ADCOCK) writes:
>Given that real-world commercial software products of typical size have
>thousands, if not tens-of-thousands of bugs discovered before shipping,...

You seem so overly predisposed to the prejudice of "programming as engineering"
as to unnecessarily exclude a concept that is already proven to work.

For example,  the program I made reference to in a previous article as already
having verified, optimized, and upgraded added to 4000 lines and the analysis
took 2 weeks.

Because of the enormous amount of knowledge of that software gathered during
the proof process, I can literally go into it and make modifications to it
in under a minute (whenever the specification is upgraded).  In fact a 200
line extension took an hour to write, and was proven bugfree before the
first run.

On another occasion, a 1000 line parser generator took one night to prove
consistent with its design, and was subsequentally coded in two days without a
single error (though the design itself had one minor easily corrected flaw).

So... size is simply not an obstacle.  It's just a matter of having the
competence to carry out such an analysis.

>Again: 'proving' that software is correct does nothing to improve the
>quality of that software.

To prove a piece of software correct means to prove that is does not have any
bugs in it (i.e. there is no inconsistency between specification and
implementation).  It also means to optimize the software using the newly found
information gathered during the proof process on its implementation, and my
experience has been that most if not all software beyond a certain scale (that
has not already undergone this type of analysis) can be optimized by at least
50% if not more (while simultaneously upgrading its functionality, readibility,
and verifiability).

In my book, showing that a piece of software has no bugs in it is a MAJOR
improvement on its quality, especially when done in conjunction with the
subsequent optimizations.  It leads major improvements in design.

In addition, when the software is encumbered by the addition of signal
processing routines and interrupts, it proves to be a NECESSITY to
verify mathematically its proper functioning.  I would consider it
irresponsible design if such software was distributed and was not verified
against race conditions and things of the like.