Coupling invariant

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.