Floyd-Hoare Verification Harmful??

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

    Date: Sat, 21 May 88 14:18:15 EDT
    From: 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

I did say that the paper was tongue in cheek and that I never circulated
it, except to friends.  The reason for the title at the time was that V.
Pratt (who was in the next office to me) claimed to have a complete
Floyd-Hoare axiom system for languages that manipulated arrays and
pointers and furthermore claimed that it was proven correct with respect
to a semantics based on Dynamic Logic.  However, both the axiom system
and the semantics had a bug similar to the one you pointed out.  I chose
such an obnoxious title as a way of chiding people about making
inflated claims for the power of their techniques.

Indeed the problem is that when allows arbitrary pointer and array
manipulations one can get aliasing problems.  It is very hard to write
an axiom set in the Floyd-Hoare tradition that does not screw up for
such languages.  There are two responses, one is to weaken the language
in such a way as to prevent aliasing.  The other is to create a
different technique stating the language axioms and verifying programs.
To date, I haven't seen a proposal in either direction that seems
workable.  Attempts to constrain pointer manipulation seem to constrain
more than you'd like.

Anyhow, I'm hardly trying to resurrect my paper.  I was just amused to
see someone pointing out the same problem after all these years.