hes@VALLECITO.SCRC.SYMBOLICS.COM (Howard Shrobe) (05/20/88)
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.gls@THINK.COM (05/21/88)
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 Now consider the array assignment Y(A[.]) := 2 . :-) --Quux
gls@THINK.COM (05/26/88)
In case anyone cares:
Date: Wed, 25 May 88 09:56:02 EDT
From: Mitchell Wand <wand@corwin.ccs.northeastern.edu>
Date: Mon, 23 May 88 18:01:34 EDT
From: gls@think.com
Date: Sat, 21 May 88 13:59:33 EDT
From: Mitchell Wand <wand@corwin.ccs.northeastern.edu>
Now consider the array assignment Y(A[.]) := 2 . :-)
Umm, I will admit my ignorance. Could you explain this joke? --Mitch
My notation was obscure, if not erroneous. By A[.] I meant the
array A considered as a unary function. So the assignment means
to change A so that its fixed point (or at least one of them) is 2.
Assuming a principle of least change, that means the same as
A[2] := 2. (Do you agree?)
I guess so. :-) --Mitch