Article View: comp.ai
Article #1229Re: Reasons why you don't prove your programs are correct
From: Flame Bait
Date: Thu, 18 Jan 1990 19:01
Date: Thu, 18 Jan 1990 19:01
16 lines
1470 bytes
1470 bytes
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
Technical Details
Message-ID:
<16773@joshua.athertn.Atherton.COM>Path:
arc1-ca.pugleaf.net!utzoo!utgpu!jarvis.csri.toronto.edu!cs.utexas.edu!swrinde!zaphod.mps.ohio-state.edu!brutus.cs.uiuc.edu!apple!voder!pyramid!athertn!joshuaReferences:
<16479@joshua.athertn.Atherton.COM> <1455@krafla.rhi.hi.is> <16665@joshua.athertn.Atherton.COM> <10289@microsoft.UUCP> <1248@oravax.UUCP>Show Full Headers
Complete Article Headers
Path: arc1-ca.pugleaf.net!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