This paper investigates data refinement by forward simulation for specifications whose semantics is given by partial relations. The most well-known example of such a semantics is that for Z. The standard model-theoretic approach is based on totalisation and lifting. The paper examines this model, exploring and isolating the precise roles played by lifting and totalisation in the standard account by introducing a simpler, normative theory of forward simulation data refinement (SF-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.
展开▼
