Maximally abstract retrenchments
Richard Banach · 2002
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.