Xref: utzoo comp.ai:5599 comp.edu:2933 comp.object:763
Path: utzoo!utgpu!jarvis.csri.toronto.edu!cs.utexas.edu!samsung!think!barmar
From: barmar@think.com (Barry Margolin)
Newsgroups: comp.ai,comp.edu,comp.object
Subject: Re: Reasons why you don't prove your programs are correct
Message-ID: <32965@news.Think.COM>
Date: 18 Jan 90 05:42:57 GMT
References: <16479@joshua.athertn.Atherton.COM> <1455@krafla.rhi.hi.is> <16665@joshua.athertn.Atherton.COM> <10289@microsoft.UUCP> <1248@oravax.UUCP>
Sender: news@Think.COM
Followup-To: comp.ai
Organization: Thinking Machines Corporation, Cambridge MA, USA
Lines: 41

In article <1248@oravax.UUCP] ian@oravax.odyssey.UUCP (Ian Sutherland) writes:
]	void swap(x,y)
]	int *x;
]	int *y;
]	{
]		int temp;
]
]		temp = *x;
]		*x = *y;
]		*y = temp;
]	}
]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.

Since the expression &temp never appears, there is no valid way to have a
pointer to temp.  It's possible to have a pointer which happens to have the
address of temp in it, but that would be due to invalid code elsewhere in
the program.  For instance, if a pointer to an automatic variable is stored
in a global variable or returned from a function then it may later point to
an automatic variable in a different function.  This is essentially the
same as using an uninitialized pointer variable.

When verifying a program, certain assumptions must be made.  People have
already pointed out that you must assume that the supporting facilities
(the compiler, the runtime library, the hardware) behave as documented, you
must also assume that a function is called validly when verifying that
function in isolation.  Otherwise, one could claim that the above function
doesn't operate properly when passed the wrong number of arguments, or when
passed integers (rather than pointers to integers), or when passed pointers
to non-integers.  Verifying the above function amounts to saying that
adding it to a correct program will not make that program incorrect.

--
Barry Margolin, Thinking Machines Corp.

barmar@think.com
{uunet,harvard}!think!barmar