Coupling invariant
= 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[0..n)=\operatorname{sort}(xs)$ and $n=\operatorname{length}(xs)$ justify constant-time indexed queries on a <sorted array>.