Abstract
It has been noticed for some time, that when refinement is used as the sole means of progressing from an abstract model to a concrete one, then certain difficulties plague the development process due to the unforgiving nature of the usual refinement proof obligations. In its familiar downward simulation setting, refinement implies two things. Firstly that whenever the abstract model is able to make a step, the concrete model must also be able to make some step. And secondly that whenever the concrete model actually makes a step, there must be an abstract step that simulates it, in order to preserve the user’s fiction, that it is the abstract model that is doing the work. The abstract model says when a step must be possible, while the concrete model dictates how the outcome may appear. This close link may be counterproductive in certain situations.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Banach, R., Poppleton, M. (1999). Retrenchment. In: Wing, J.M., Woodcock, J., Davies, J. (eds) FM’99 — Formal Methods. FM 1999. Lecture Notes in Computer Science, vol 1709. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48118-4_56
Download citation
DOI: https://doi.org/10.1007/3-540-48118-4_56
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66588-5
Online ISBN: 978-3-540-48118-8
eBook Packages: Springer Book Archive