The Community for Technology Leaders
Formal Engineering Methods, International Conference on (2000)
York, England
Sept. 4, 2000 to Sept. 7, 2000
ISBN: 0-7695-0822-7
pp: 133
R. Banach , Manchester University
ABSTRACT
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 pre-formal 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 are briefly explored.
INDEX TERMS
CITATION

R. Banach, "Maximally Abstract Retrenchments," Formal Engineering Methods, International Conference on(ICFEM), York, England, 2000, pp. 133.
doi:10.1109/ICFEM.2000.873813
90 ms
(Ver 3.3 (11022016))