Constraints: A Uniform Approach to Aliasing and Typing

My generalized Hoare logic requires reasoning about control predicates, using the at, in, and after predicates introduced in [47]. These are not independent predicates–for example, being after one statement is synonymous with being at the following statement. At some point, Schneider and I realized that the relations between control predicates could be viewed as a generalized form of aliasing. Our method of dealing with control predicates led to a general approach for handling aliasing in ordinary Hoare logic, which is described in this paper. In addition to handling the usual aliasing in programs, our method allowed one to declare that the variables r and theta were aliases of the variables x and y according to the relations x = r * cos(theta) and y = r * sin(theta).

We generalized this work to handle arrays and pointers, and even cited a later paper about this generalization. But, as has happened so often when I write a paper that mentions a future one, the future paper was never written.