Re: ''Update functions'' in Scheme.

[Howard Shrobe <hes@VALLECITO.SCRC.Symbolics.COM>]

    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.