Filtering Retrenchments into Refinements

Retrenchment is a weakening of model based refinement that enables many development steps not expressible by refinement to be formally described nevertheless. The greater flexibility of retrenchment comes at the price of much feebler guarantees as compared with refinement, and so the interplay between retrenchment and refinement can hope to offer the best of both worlds. The paper explores the strategy of filtering the information in a retrenchment to yield a refinement under a suitable notion of observation. A general construction is given that enables a retrenchment, with its intrinsic notion of observability, to be filtered to produce a refinement with its intrinsic notion of observability. A simple running example illustrates the theory