[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: ''Update functions'' in Scheme.
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] := 2
in a two element array A, where initially A=A=1 . This sort of thing had
program verifiers confused for a good while in the early 70's.
College of Computer Science
360 Huntington Avenue #161CN
Boston, MA 02115
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.