Path: utzoo!utgpu!water!watmath!clyde!att!osu-cis!tut.cis.ohio-state.edu!bloom-beacon!VALLECITO.SCRC.SYMBOLICS.COM!hes
From: hes@VALLECITO.SCRC.SYMBOLICS.COM (Howard Shrobe)
Newsgroups: comp.lang.scheme
Subject: Re: ''Update functions'' in Scheme.
Message-ID: <19880520165408.4.HES@MERLIN.SCRC.Symbolics.COM>
Date: 20 May 88 16:54:00 GMT
References: <8805191435.AA16901@corwin.CCS.Northeastern.EDU>
Sender: daemon@bloom-beacon.MIT.EDU
Organization: The Internet
Lines: 30


    Date: Thu, 19 May 88 10:35:23 EDT
    From: Mitchell Wand <wand%corwin.ccs.northeastern.edu@RELAY.CS.NET>

    One ought not to say things like:

    "F(G(C)) := D ought to ensure that F(G(C)) = D afterwards."

    too blithely.  Consider the array assignment:

    A[A[1]] := 2

    in a two element array A, where initially A[1]=A[2]=1 .  This sort of thing had
    program verifiers confused for a good while in the early 70's.


    Mitchell Wand
    College of Computer Science
    Northeastern University
    360 Huntington Avenue #161CN
    Boston, MA 02115

    CSNet:  wand@corwin.ccs.northeastern.edu


I wrote a paper that was distributed by hand to friends in the late '70s
called "Floyd-Hoare Verifiers Considered Harmful" that pointed this
ought.  It was somewhat tongue in cheek but was based on catching Vaughn
Pratt making exactly this kind of mistake.  I just moved my office and
found copies of the paper.  Sussman would remember it well.