Towards pointer algebra (Q685621)

Algorithms involving pointers are difficult to write and to verify. Due to the implicit connections through paths within a pointer structure, the side effects of a pointer assignment are much harder to survey than those of an assignment to a simple variable. Second, a careless assignment may destroy the last link to a substructure which thus is lost forever. Such errors are easily made, but found only with difficulty. The paper presents an approach to improving the situation. The store, which is an implicit global parameter in procedural languages, is made into an explicit parameter. This allows passing to an applicative treatment using a suitable algebra of operations on the store. The storage state of a von Neumann machine can be viewed as a total map from addresses to certain values. A part of such a state that forms a logical unit can then be represented by a partial submap of that map. So the state can be described in a modular way as the union of the submaps for its logical subunits. Therefore we use the algebra of relations and partial maps as our tool for specifying and developing of relational overwriting which in the case of partial maps models storage updates. The properties of overwriting are proved within abstract relational algebra. In connection with the algebra of partial maps the well-known unfold/fold transformation strategy is used for the (formal) derivation of correct pointer algorithms. This is illustrated with two algorithms on singly linked lists, viz. concatenation and reversal ``in situ''. The approach extends well to arbitrary pointer structures.