Abstract
Retrenchment is introduced as a liberalisation of refinement intended to address some of the shortcomings of refinement as sole means of progressing from simple abstract models to more complex and realistic ones. In retrenchment the relationship between an abstract operation and its concrete counterpart is mediated by extra predicates, allowing the expression of non-refinement-like properties and the mixing of I/O and state aspects in the passage between levels of abstraction. Modulated refinement is introduced as a version of refinement allowing mixing of I/O and state aspects, in order to facilitate comparison between retrenchment and refinement, and various notions of simulation are considered in this context. Stepwise simulation, the ability of the simulator to mimic a sequence of execution steps of the simulatee in a sequence of equal length is proposed as the benchmark semantic notion for relating concepts in this area. One version of modulated refinement is shown to have particularly strong connections with automata theoretic strong simulation, in which states and step labels are mapped independently from simulator to simulatee. A special case of retrenchment, simple simulable retrenchment is introduced, and shown to have properties very close to those of modulated refinement. The more general situation is discussed briefly. The details of the theory are worked out for the B-Method, though the applicability of the underlying ideas is not limited to just that formalism.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Banach R., Poppleton M. Retrenchment: An Engineering Variation on Refinement. in: Proc. B-98, Bert (ed.), Springer, 1998, 129–147, LNCS 1393. See also: UMCS Technical Report UMCS-99-3-2, http://www.cs.man.ac.uk/cstechrep
Abrial J.R. The B-Book. Cambridge University Press, 1996.
Wordsworth J.B. Software Engineering with B. Addison-Wesley, 1996.
Lano K., Haughton H. Specification in B: An Introduction Using the B-Toolkit. Imperial College Press, 1996.
Sekerinski E., Sere K. Program Development by Refinement: Case Studies Using the B Method. Springer, 1998.
Hayes I. J., Sanders J. W. Specification by Interface Separation. Form. Asp. Comp. 7, 430–439, 1995.
Mikhajlova A, Sekerinski E. Class Refinement and Interface Refinement in Object-Oriented Programs. in: Proc. FME-97, Fitzgerald, Jones, Lucas (eds.), Springer, 1997, 82–101, LNCS 1313.
Boiten E., Derrick J. IO-Refinement in Z. in: Proc. Third BCS-FACS Northern Formal Methods Workshop. Ilkley, U.K., BCS, 1998, http://www.ewic.org.uk/ewic/ workshop/view.cfm/NFM-98
Stepney S., Cooper D., Woodcock J. More Powerful Z Data Refinement: Pushing the State of the Art in Industrial Refinement. in: Proc. ZUM-98, Bowen, Fett, Hinchey (eds.), Springer, 1998, 284–307, LNCS 1493.
Back R. J. R., Kurki-Suonio R. Decentralisation of Process Nets with Centralised Control. in: Proc. 2nd ACM SIGACT-SIGOPS Symp. on Princ. Dist. Comp., 131–142, ACM, 1983.
Back R. J. R. Refinement Calculus Part II: Parallel and Reactive Systems. in: Proc. REX Workshop, Stepwise Refinement of Distributed Systems, de Roever, Rozenberg (eds.), Springer, 1989, 67–93, LNCS 430.
Back R. J. R., von Wright J. Trace Refinement of Action Systems. in: Proc. CONCUR-94, Jonsson, Parrow (eds.), Springer, 1994, 367–384, LNCS 836.
Francez N., Forman I. R. Superimposition for Interactive Processes. in: Proc. CONCUR-90, Baeten, Klop (eds.), Springer, 1990, 230–245, LNCS 458.
Katz S. A Superimposition Control Construct for Distributed Systems. ACM Trans. Prog. Lang. Sys. 15, 337–356, 1993.
Back R. J. R., Sere K. Superposition Refinement of Reactive Systems. Form. Asp. Comp. 8, 324–346, 1996.
Blikle A. The Clean Termination of Iterative Programs. Acta Inf. 16, 199–217, 1981.
Coleman D., Hughes J. W. The Clean Termination of Pascal Programs. Acta Inf. 11, 195–210, 1979.
Neilson D. S. From Z to C: Illustration of a Rigorous Development Method. PhD. Thesis, Oxford University Computing Laboratory Programming Research Group, Technical Monograph PRG-101, 1990.
Owe O. An Approach to Program Reasoning Based on a First Order Logic for Partial Functions. University of Oslo Institute of Informatics Research Report No. 89. ISBN 82-90230-88-5, 1985.
Owe O. Partial Logics Reconsidered: A Conservative Approach. Form. Asp. Comp. 3, 1–16, 1993.
Jonsson B. Simulations between Specifications of Distributed Systems. in: Proc. CONCUR-91, Baeten, Groote (eds.), Springer, 1991, 346–360, LNCS 527.
Abadi M., Lamport L. The Existence of Refinement Mappings. Theor. Comp. Sci. 82, 253–284, 1991.
Jonsson B. On Decomposing and Refining Specifications of Distributed Systems. in: Proc. REX Workshop, Stepwise Refinement of Distributed Systems, de Roever, Rozenberg (eds.), Springer, 1989, 361–385, LNCS 430.
Lynch N. Multivalued Possibilities Mappings. in: Proc. REX Workshop, Stepwise Refinement of Distributed Systems, de Roever, Rozenberg (eds.), Springer, 1989, 519–543, LNCS 430.
Merritt M. Completeness Theorems for Automata. in: Proc. REX Workshop, Stepwise Refinement of Distributed Systems, de Roever, Rozenberg (eds.), Springer, 1989, 544–560, LNCS 430.
Banach R., Poppleton M. Retrenchment and Punctured Simulation. in: Proc. IFM-99, Taguchi, Galloway (eds.), 457–476, Springer, 1999.
Derrick J., Bowman H., Boiten E., Steen M. Comparing LOTOS and Z Refinement Relations. in: Proc. FORTE/PSTV-9, 501–516, Chapman and Hall, 1996.
Bolton C, Davies J., Woodcock J. On the Refinement and Simulation of Data Types and Processes. in: Proc. IFM-99, Taguchi, Galloway (eds.), 273–292, Springer, 1999.
Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Banach, R., Poppleton, M. (2000). Retrenchment, Refinement, and Simulation. In: ZB 2000: Formal Specification and Development in Z and B. ZB 2000. Lecture Notes in Computer Science, vol 1878. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44525-0_18
Download citation
DOI: https://doi.org/10.1007/3-540-44525-0_18
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67944-8
Online ISBN: 978-3-540-44525-8
eBook Packages: Springer Book Archive