Calculating with pointers.

Abstract

This note presents a calculational method for dealing with pointers in weakest precondition semantics. It aims at facilitating the verification of program fragments that use pointers, without recourse to operational reasoning. It is true that the unrestricted use of pointers may be considered somewhat oldfashioned. There is a growing consensus (to which the present author subscribes) that the derivation of correct programs is much to be preferred over any a posteriori verification. Types such as lists and trees have mathematical properties that are simpler than those of pointers, hence are more useful in program derivation. Recent publications concerning pointers typically propose schemes for their abolition [6, 7]. Nevertheless the study of pointers retains some importance, because the more abstract types are usually implemented by means of pointers and one wishes to prove the correctness of such an implementation. Moreover, there exist algorithms that exploit the aliasing effect provided by pointers for efficiency reasons [3].