*This chapter is concerned with proving correctness of ADT implementations by
exhibiting a simulation relation between a reference implementation (taken, or known, to
be correct) and a candidate implementation (whose correctness is to be established).
The methodology generalizes Hoare's notion of abstraction functions to an arbitrary
relation, and relies on Reynolds' notion of parametricity to conclude that related
implementations engender the same observable behavior in all clients.*