Calculational derivation of pointer algorithms from tree operations

摘要

We describe an approach to the derivation of correct algorithms on tree-based pointer struc- tures. 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 sim- ple syntactic restrictions on transformable programs.