Sharp retrenchment, modulated refinement and simulation

Sharp retrenchment is introduced and briefly justified informally, as a liberalisation of refinement. In sharp retrenchment the relationship between an abstract operation and its concrete counterpart is mediated by extra predicates, allowing most particularly the description of non-refinement-like properties, and the mixing of I/O and state aspects in the passage between levels of abstraction. Sharp retrenchments are briefly contrasted with unsharp ones. Sharp retrenchments are shown to have a natural law of composition, and the way in which refinements may be viewed as sharp retrenchments is discussed. Modulated refinement is introduced as a version of refinement allowing mixing of I/O and state aspects, in order to facilitate comparison between sharp retrenchment and refinement, and various notions of simulation are considered in this context, specifically: stepwise simulation, the ability of simulator to mimic a sequence of execution steps of the simulatee; strong simulation, in which states and step labels are mapped independently between simulatee and simulator; and the refinement notion itself. Special cases of sharp retrenchment are shown to possess various subsets of these simulation properties, and the extent to which sharp retrenchments contain refinements within them is addressed. The details of the theory are worked out for the B-Method, though the applicability of the underlying ideas is not limited to just that formalism.