Retrenchment and Punctured Simulation

: Some of the shortcomings of using refinement alone as the means of passing from high level simple models to actual detailed implementations are reviewed. Retrenchment is presented as a framework for ameliorating these. In retrenchment the relationship between an 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 in the passage between levels of abstraction. Stepwise simulation, the ability of simulator to mimic a sequence of execution steps of the simulatee, is introduced as the reference point for discussing the broader semantic issues surrounding retrenchment. Punctured simulation is introduced as a naturally occurring phenomenon implicit in the ability of retrenchments to describe of non-refinement-like properties; and it is shown to have relevance even in some refinements. Two special cases of retrenchment, simple simulable retrenchment and memoryles...

• Type: Conference
• Year: 1999
• Where: IFM
• Authors: Richard Banach, Michael Poppleton
• Keywords: Formal Methods, IFM 1999, Issues Surrounding Retrenchment, Retrenchment, Simple Simulable Retrenchment