Abstract
Previous chapters have considered refinement in terms of upward and downward simulations, which are sound and jointly complete—i.e., all refinements can be proved using a combination of upward and downward simulation steps. This chapter presents an alternative in the form of powersimulations which provide for a single complete refinement rule for Z. This requires a change in the underlying framework, moving from relations to possibility mappings.
Excerpts from pp. 2, 5–12 of [4] are reprinted within this chapter by permission from Oxford University Press.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsReferences
Abadi, M., & Lamport, L. (1991). The existence of refinement mappings. Theoretical Computer Science, 2(82), 253–284.
de Bakker, J. W., de Roever, W.-P., & Rozenberg, G. (Eds.) (1990). REX Workshop on Stepwise Refinement of Distributed Systems, Nijmegen, 1989. Lecture Notes in Computer Science: Vol. 430. Berlin: Springer.
de Roever, W.-P., & Engelhardt, K. (1998). Data Refinement: Model-Oriented Proof Methods and Their Comparison. Cambridge: Cambridge University Press.
Derrick, J. (2000). A single complete refinement rule for Z. Journal of Logic and Computation, 10(5), 663–675.
Gardiner, P. H. B., & Morgan, C. C. (1993). A single complete rule for data refinement. Formal Aspects of Computing, 5, 367–382.
Gerth, R. (1990) Foundations of compositional program refinement. In de Bakker et al. [2] (pp. 777–807).
Lynch, N. A. (1990) Multivalued possibility mappings. In de Bakker et al. [2] (pp. 519–543).
Lynch, N. A., & Vaandrager, F. (1992). Forward and backward simulations for timing-based systems. In J. W. de Bakker, W.-P. de Roever, C. Huizing, & G. Rozenberg (Eds.), Real-Time: Theory in Practice, REX Workshop, Mook, The Netherlands, June 1991. Lecture Notes in Computer Science: Vol. 600 (pp. 397–446). Berlin: Springer.
Merritt, M. (1990) Completeness theorems for automata. In de Bakker et al. [2] (pp. 544–560).
Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer-Verlag London
About this chapter
Cite this chapter
Derrick, J., Boiten, E.A. (2014). A Single Simulation Rule. In: Refinement in Z and Object-Z. Springer, London. https://doi.org/10.1007/978-1-4471-5355-9_8
Download citation
DOI: https://doi.org/10.1007/978-1-4471-5355-9_8
Publisher Name: Springer, London
Print ISBN: 978-1-4471-5354-2
Online ISBN: 978-1-4471-5355-9
eBook Packages: Computer ScienceComputer Science (R0)