Author: Lindsay Groves
Source: GZipped PostScript (43kb); Adobe PDF (260kb)
Many computing problems can be described as a composition of two relations (or functions) linked by an intermediate data structure, such as a list or set. In the interests of separation of concerns and reuse of general techniques, it is often desirable to implement the two relations separately and combine their implementations. In the interests of efficiency, however, it is often desirable to eliminate the intermediate data structure from the implementation, and this is vital in cases where the intermediate structure is infinite. Various techniques have been developed for eliminating (or at least restricting) intermediate structures in functional and logic programs, including the use of special execution mechanisms (e.g. lazy evaluation and coroutining of goals) and fold/unfold transformations. In formal derivation of imperative programs it appears more common to consider both relations together from the outset, with consequent loss of separation of concerns and reusability of general derivations.
In this paper, we show that intermediate data structures can be eliminated using data refinement. This allows separate relations in the specification to be considered separately in deriving an algorithm, while still arriving at an efficient implementation. It is hoped that this will make it easier to reuse general derivation strategies.