Calculational Derivation of Algorithms on Tree-based Pointer Structures

We describe an approach to the derivation of correct algorithms on tree-based pointer structures. The approach is based on identifying abstract representations of commonly used pointer manipulations on trees and providing calculational-style refinement rules for these manipulations. This allows the algorithmic structure of a program to be derived using abstract data representations before introducing pointer structures.