An analysis of backward simulation data-refinement for partial relation semantics

We investigate data-refinement by backward simulation for specifications whose semantics is given by partial relations. The standard model-theoretic approach is based on totalisation and lifting. We examine this model, exploring and isolating the precise roles played by lifting and totalisation in the standard account by introducing a simpler, normative theory of backward simulation data-refinement (SB-refinement) which captures refinement directly in the language and in terms of the natural properties of preconditions and postconditions. This theory is used in conjunction with four other model-theoretic approaches to determine the extent to which the standard approach is canonical, and the extent to which it is arbitrary.