wand@corwin.ccs.northeastern.EDU (Mitchell Wand) (05/22/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. 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
hes@VALLECITO.SCRC.SYMBOLICS.COM (Howard Shrobe) (05/24/88)
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.
reddy@REDDY.CS.UIUC.EDU (Uday S. Reddy) (05/28/88)
Howard Shrobe: 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. Well, that depends on what you mean by "workable". The standard technique used for handling aliasing (for example, in denotational semantics) is a two-level store. The first level called "environment" binds variables to objects, and the second level called "store" binds objects to values. We then have an accurate semantic formulation, but reasoning is harder than in Floyd-Hoare tradition. A two-level store formulation in predicate logic style is the recent "situational calculus" semantics of Manna and Waldinger. It remains to be seen how nice reasoning looks like in this framework. Another technique, attributed to Landin, is to use an "equivalence relation" on variables. Modifying any variable in an equivalence class has the effect of modifying all the variables in the class. Reasoning seems to be nicer in this framework. But, one has to be careful about the order of evaluation. A version of the Church-Rosser property gets lost when aliasing is introduced. Uday Reddy