Floyd-Hoare Verification Harmful??

[Mitchell Wand <wand%corwin.ccs.northeastern.edu@RELAY.CS.NET>]

       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.

   Date: Fri, 20 May 88 12:54 EDT
   From: Howard Shrobe <hes@scrc-vallecito.arpa>

   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.

That seems like an awfully rash conclusion to draw from this kind of bug.  It
would be more reasonable to say something like "Unrestricted Pointer
Manipulation Considered Harmful" or "Hiding Nasty Pointer Manipulation in
Innocuous-Looking Array Manipulation Considered Harmful" or... :-)

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

CSNet:  wand@corwin.ccs.northeastern.edu