Floyd-Hoare Verification Harmful??

[reddy%reddy.cs.uiuc.edu@a.cs.uiuc.edu (Uday S. Reddy)]

   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