Calculational derivation of pointer algorithms from tree operations

We describe an approach to the derivation of correct algorithms on tree-based pointer structures. The approach is based on enriching trees in a way that allows us to model commonly used pointer manipulations on tree structures. We provide rules which allow recursive functions on trees to be transformed into imperative algorithms on enriched trees. In addition, we provide rules which allow algorithms on enriched trees to be mechanically transformed into efficient pointer algorithms. All transformations are correctness-preserving. A key point of our approach is that we avoid aliasing through the way in which trees are enriched and through some simple syntactic restrictions on transformable programs.