Xref: utzoo comp.ai:5615 comp.edu:2937 comp.object:773
Path: utzoo!utgpu!jarvis.csri.toronto.edu!cs.utexas.edu!swrinde!zaphod.mps.ohio-state.edu!brutus.cs.uiuc.edu!apple!voder!pyramid!athertn!joshua
From: joshua@athertn.Atherton.COM (Flame Bait)
Newsgroups: comp.ai,comp.edu,comp.object
Subject: Re: Reasons why you don't prove your programs are correct
Message-ID: <16773@joshua.athertn.Atherton.COM>
Date: 18 Jan 90 19:01:12 GMT
References: <16479@joshua.athertn.Atherton.COM> <1455@krafla.rhi.hi.is> <16665@joshua.athertn.Atherton.COM> <10289@microsoft.UUCP> <1248@oravax.UUCP>
Reply-To: joshua@Atherton.COM (Flame Bait)
Organization: Atherton Technology, Sunnyvale, CA
Lines: 16

This is a reply to article <1248@oravax.UUCP> ian@oravax.odyssey.UUCP,
written by Ian Sutherland.  Please look at that posting to see his bogus
example.

Ian:  please learn C (and teach it to your proof system) before posting
examples using it.  In your example temp is an automatic (or local)
variable, while a and b are parameters passed into the function which
contains temp.  There is no way in C for temp to be the same variable
as either a or b.  If temp were a static or a global, there would be
a problem.  Note that calling swap recursively will work fine given 
your example.  

This all assumes a working compiler, linker, and runtime, of course.

Joshua Levy                          joshua@atherton.com  home:(415)968-3718
                        {decwrl|sun|hpda}!athertn!joshua  work:(408)734-9822