Abstract
This chapter introduces the notion of refinement informally, and discusses the refinement of operations on a given data type. We first present a semi-formal motivation of the simplest refinement relation of all, namely operation refinement. Operation refinement can be applied to individual operations without reference to the other operations present in the abstract data type (ADT). The other simple refinement rules presented in this chapter, establishing and imposing invariants, only apply in the context of a full ADT, and require abstraction, in the sense of the state not being observable.
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
Notes
- 1.
On the other hand, replacing the machine that performs the weekly lottery draw with one which returns the same set of numbers every week is probably not an acceptable refinement. This requires a more sophisticated explanation, however, concerning the difference between non-deterministic and probabilistic choice, which is outside the scope of this book—see [5] for a comprehensive treatment.
- 2.
A partial order ≤ is a pre-congruence if for all contexts C[.], whenever x≤y also C[x]≤C[y].
- 3.
Minus the obvious case for the empty sequence.
- 4.
Note, however, that given this definition of observations, it is impossible to define COp such that (x,⊥) is a possible observation but not (x,y) for some y.
- 5.
In other words, by having the single operation Travel as its interface, our ADT does not express the level of external choice that would be necessary from the customer’s point of view.
- 6.
At the time of writing, there were actually very few such stations.
References
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 Nicola, R. (1987). Extensional equivalences for transition systems. Acta Informatica, 24(2), 211–237.
de Roever, W.-P., & Engelhardt, K. (1998). Data Refinement: Model-Oriented Proof Methods and Their Comparison. Cambridge: Cambridge University Press.
Gardiner, P. H. B., & Morgan, C. C. (1993). A single complete rule for data refinement. Formal Aspects of Computing, 5, 367–382.
McIver, A., & Morgan, C. C. (2004). Abstraction, Refinement and Proof for Probabilistic Systems. Berlin: Springer.
Nipkow, T. (1990) Formal verification of data type refinement—theory and practice. In de Bakker et al. [1] (pp. 561–591).
Reeves, S., & Streader, D. (2011). Contexts, refinement and determinism. Science of Computer Programming, 76(9), 774–791.
Strulo, B. (1995). Email communication.
van Glabbeek, R. J. (1993). The linear time–branching time spectrum II. The semantics of sequential systems with silent moves (extended abstract). In E. Best (Ed.), CONCUR’93, 4th International Conference on Concurrency Theory. Lecture Notes in Computer Science: Vol. 715 (pp. 66–81). Berlin: Springer.
van Glabbeek, R. J. (2001). The linear time–branching time spectrum I. The semantics of concrete sequential processes. In J. A. Bergstra, A. Ponse, & S. A. Smolka (Eds.), Handbook of Process Algebra (pp. 3–99). Amsterdam: North-Holland.
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). Simple Refinement. In: Refinement in Z and Object-Z. Springer, London. https://doi.org/10.1007/978-1-4471-5355-9_2
Download citation
DOI: https://doi.org/10.1007/978-1-4471-5355-9_2
Publisher Name: Springer, London
Print ISBN: 978-1-4471-5354-2
Online ISBN: 978-1-4471-5355-9
eBook Packages: Computer ScienceComputer Science (R0)