Data refinement
= 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.