Data refinement

Implementation of an abstract state and operations using a more concrete representation, justified by a coupling invariant. For example, an insertion-history list may be implemented by a sorted array when clients observe only occurrence counts and order statistics. The observable behavior, rather than insertion order internally, must agree.

A relation between abstract and concrete states used to prove data refinement. Establish it initially; show that each concrete operation simulates the specified abstract operation and restores the relation; show that returned observations agree. For a rank collection, $u[\mathrm{0..}n)=\mathrm{sort}(xs)$ and $n=\mathrm{length}(xs)$ justify constant-time indexed queries on a sorted array.