[comp.misc] RE^2 Why you do not prove your programs correct

pontius@ficc.uu.net (terry pontius) (01/18/90)

One point this thread seems to ignore is that Software Quality is not
just about 'correctness'. 

Maintenance and modification are subjects which also must be addressed. 

A program written for a real-world application is just about useless 
if it can't be maintained or modified, correct or not!

To my mind, a verifier can only do about half the job of testing.
It can prove the program does what it was designed to do.  What verifiers
do not generally do is prove the program does not do what it is not 
supposed to do.

A Verifier which verifies a 4000 line chunk of code as "bug free" should 
be highly suspect (IMHO).  
Does this program still function normally if some of its inputs are 
grossly out of valid ranges?  What happens when an interface provides 
data that "can't happen"?  Verifiers typically don't check for those kinds
of errors in a reasonable amount of time.

The attitude in this thread seems to be that a Specification is chiseled 
in stone before the designer/programmer sees it, and therefore, a verifier
need only prove the specification.  If you write software that only barely 
meets spec., you better plan for another vocation real soon.  

Software designs have to be able to take hits from spec changes and absorb
modifications without creating more problems than are solved.  
Verifiers can't measure this ability very effectively, if at all.

The term "Verify" has positive connotations, and yet software testing is
an essentially negative exercise.  The designer's function is 'creative'; 
the testor's function is 'destructive'.  The designer succeeds when the
program works; the testor succeeds when the program breaks.  The successful
development team experiences alot of success on both sides, because
every defect the testor is able to find, is a defect the client will
never see.  IMHO, a testor who cannot find a defect is not doing his job.

T L Pontius 
Applied Technology Associates
Houston