Retrenchment is introduced as a liberalisation of refinement intended to address some of the shortcomings of refinement as sole means of progressing from simple abstract models to more complex and realistic ones. In retrenchment the relationship between an abstract operation and its concrete counterpart is mediated by extra predicates, allowing the expression of non- refinement-like properties and the mixing of I/O and state aspects in the passage between levels of abstraction. Modulated refinement is introduced as a version of refinement allowing mixing of I/O and state aspects, in order to facilitate comparison between retrenchment and refinement, and various notions of simulation are considered in this context. Step-wise simulation, the ability of the simulator to mimic a sequence of execution steps of the simulatee in a sequence of equal length is proposed as the benchmark semantic notion for relating concepts in this area. One version of modulated refinement is shown to have particularly strong connections with automata theoretic strong simulation, in which states and step labels are mapped independently from simulator to simulatee. A special case of retrenchment, simple simulable retrenchment is introduced, and shown to have properties very close to those of modulated refinement. The more general situation is discussed briefly. 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.
展开▼
