Abstract
It is argued that refinement, in which I/O signatures stay the same, preconditions are weakened and postconditions strengthened, is too restrictive to describe all but a fraction of many realistic developments. An alternative notion is proposed called retrenchment, which allows information to migrate between I/O and state aspects of operations at different levels of abstraction, and which allows only a fraction of the high level behaviour to be captured at the low level. This permits more of the informal aspects of design to be formally captured and checked. The details are worked out for the B-Method.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Abadi M., Lamport L. (1991); The Existence of Refinement Mappings. Theor. Comp. Sci. 82, 153–284.
Abrial J. R. (1996); The B-Book. Cambridge University Press.
Alur R., Henzinger T., Sontag E. (eds.) (1996); Hybrid Systems III: Verification and Control. LNCS 1066, Springer.
Back R. J. R. (1981); On Correct Refinement of Programs. J. Comp. Sys. Sci. 23, 49–68.
Back R. J. R. (1988); A Calculus of Refinements for Program Derivations. Acta Inf. 25, 593–624.
Back R. J. R., von Wright J. (1989); Refinement Calculus Part I: Sequential Nondeterministic Programs. in: Proc. REX Workshop, Stepwise Refinement of Distributed Systems, de Roever, Rozenberg (eds.), LNCS 430, 42–66, Springer.
Cunningham J. R. (1989); Development of Computer Algorithms for Radiation Treatment Planning. Int. J. Rad. Onc. Biol. Phys., 16, 1367–1376.
Harrison J. R. (1996); Theorem Proving with the Real Numbers. PhD. Thesis, Cambridge University Computing Laboratory, also Cambridge University Computing Laboratory Technical Report No. 408.
Hayes I. J. (1993); Specification Case Studies. (2nd ed.), Prentice-Hall.
Hayes I. J., Sanders J. W. (1995); Specification by Interface Separation. Form. Asp. Comp. 7, 430–439.
Hounsell A. R., Wilkinson J. M. (1994); Dose Calculations in Multi-Leaf Collimator Fields. in: Proc. XIth Int. Conf. on the use of Computers in Radiation Therapy, Manchester, UK.
Huang K. (1963); Statistical Mechanics. John Wiley.
Johns, H. E., Cunningham J. R. (1976); The Physics of Radiology. Charles C. Thomas.
Jones C. B. (1990); Systematic Software Development Using VDM. (2nd ed.), Prentice-Hall.
Jones C. B., Shaw R. C. (1990); Case Studies in Systematic Software Development. Prentice-Hall.
Khan F. M. (1994); The Physics of Radiation Therapy. Williams & Wilkins.
Lano K., Haughton H. (1996); Specification in B: An Introduction Using the B-Toolkit. Imperial College Press.
Maler O. (ed.) (1997); Hybrid and Real-Time Systems. LNCS 1201, Springer.
Morgan C. (1994); Programming from Specifications. Prentice-Hall.
Morris J. M. (1987); A Theoretical Basis for Stepwise Refinement and the Programming Calculus. Sci. Comp. Prog. 9, 287–306.
Spivey J. M. (1993); The Z Notation: A Reference Manual. (2nd ed.), Prentice-Hall.
Wand I., Milner R. (eds.) (1996); Computing Tomorrow. Cambridge University Press.
Wordsworth J. B. (1996); Software Engineering with B. Addison-Wesley
von Wright J. (1994); The Lattice of Data Refinement. Acta Inf. 31, 105–135.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Banach, R., Poppleton, M. (1998). Retrenchment: An engineering variation on refinement. In: Bert, D. (eds) B’98: Recent Advances in the Development and Use of the B Method. B 1998. Lecture Notes in Computer Science, vol 1393. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0053358
Download citation
DOI: https://doi.org/10.1007/BFb0053358
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64405-7
Online ISBN: 978-3-540-69769-5
eBook Packages: Springer Book Archive