Xref: utzoo comp.ai:5577 comp.edu:2923 comp.object:754
Path: utzoo!utgpu!jarvis.csri.toronto.edu!clyde.concordia.ca!uunet!mailrus!cornell!oravax!ian
From: ian@oravax.UUCP (Ian Sutherland)
Newsgroups: comp.ai,comp.edu,comp.object
Subject: Re: Reasons why you don't prove your programs are correct
Message-ID: <1248@oravax.UUCP>
Date: 16 Jan 90 19:42:54 GMT
References: <16479@joshua.athertn.Atherton.COM> <1455@krafla.rhi.hi.is> <16665@joshua.athertn.Atherton.COM> <10289@microsoft.UUCP>
Reply-To: ian@oravax.odyssey.UUCP (Ian Sutherland)
Organization: Odyssey Research Associates, Ithaca, New York
Lines: 46

In article <10289@microsoft.UUCP> jimad@microsoft.UUCP (JAMES ADCOCK) writes:
>The way one discovers bugs in one's software is not by trying to prove its
>correct, but rather by trying to show it is incorrect, and how.  Trying to
>'prove' software is correct does nothing to improve the quality of the software
>involved.  Finding and removing bugs does.

I have found bugs in software by trying to prove it's correct.  In the
course of trying to prove it's correct, you realize at some point that
it is NOT correct, and the failure of the proof actually points out
the bug.  Here's a simple but amusing example.  Consider the following
C program which is intended to swap the values in 2 integer locations:

	void swap(x,y)
	int *x;
	int *y;
	{
		int temp;

		temp = *x;
		*x = *y;
		*y = temp;
	}

Looks correct, doesn't it?  I tried to verify this program as a simple
example in a C verification system we built at the company I work for.
In the course of trying to verify it, I started seeing various
expressions being generated of the form "if the value in x and the
location of temp are the same then A else B".  I thought this was a bug
in the verifier until I realized that there's nothing about the above
program which ensures that swap is not passed a pointer to the location
where temp gets put.  In fact, once you think about this, it turns out
to be pretty easy to get this bug to manifest itself.  In other words,
the above program does not correctly swap the contents of the 2
locations it's passed in all cases.  Not only did attempting to verify
the program turn up this bug, but it told us exactly under what
circumstances the program will malfunction.  It's my experience that
verification not only helps you find bugs, but helps you find the ones
that you'd be least likely to find by other methods.  It's not
economical to use on large systems at the moment, but it's getting
there, and there are plenty of programs which are not so large whose
correctness is nonetheless critical to the system they're a part of.

-- 
Ian Sutherland		ian%oravax.uucp@cu-arpa.cs.cornell.edu

Sans Peur