Maximally abstract retrenchments

The more obvious and well known drawbacks of using refinement as the sole means of progressing from an abstract model to a concrete implementation are reviewed. Retrenchment is presented in a simple partial correctness framework as a more flexible development concept for formally capturing the early and otherwise preformal stages of development, and briefly justified. Given a retrenchment from an abstract to a concrete model, the problem of finding a model at the level of abstraction of the abstract model, but refinable to the concrete one, is examined. A construction is given that solves the problem in a universal manner, there being a canonical factorisation of the original retrenchment, into a retrenchment to the universal system followed by an I/O-filtered refinement. The universality amounts to the observation that the retrenchment component of any similar factorisation, factors uniquely through the universal model. The construction´s claim to be at the right level of abstraction is supported by an idempotence property. The consequences of including termination criteria in the formal models is briefly explored