Abstract
In Chap. 1 we introduced differing notions of refinement in the LTS setting - each one based upon a different notion of observation. In Chap. 2 we focused on simulations as a means to verify trace refinements in an Automata context, and we discussed both finite trace refinement as well as trace refinement in the presence of infinite traces. In Chap. 3 we developed a basic refinement model that looked at states in the first place, and constructed a relational semantics for it. We ended with sketching how labels on transitions could be added to that and how we could apply abstraction to state spaces, in preparation for the model in the current chapter. In this chapter we will look at a semantic model that is entirely based on relations and abstract state as a model of computation. In this context programs will be finite relational compositions of operations together with a finalisation which makes explicit the observations made of that program. As in Chap. 1 and ever since refinement will be the consistency of observations. We will then explore, without fixing the exact observations to be made, how simulations can be used to verify the refinement in a way similar to that found in Chap. 2.
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.
Their embedding is not explicit, instead they characterise relations in its image axiomatically.
References
Boiten EA, Derrick J (2010) Incompleteness of relational simulations in the blocking paradigm. Sci Comput Program 75(12):1262–1269
He Jifeng, Hoare CAR, Sanders JW (1986) Data refinement refined. In: Robinet B, Wilhelm R (eds) Proceedings of the ESOP 86. Lecture notes in computer science, vol 213. Springer, Berlin, pp 187–196
Woodcock JCP, Davies J (1996) Using Z: specification, refinement, and proof. Prentice Hall, Upper Saddle River
Derrick J, Boiten EA (2014) Refinement in Z and object-Z, 2nd edn. Springer, Berlin
He Jifeng, Hoare CAR (1990) Prespecification and data refinement. Data refinement in a categorical setting, Technical monograph, number PRG-90. Oxford University Computing Laboratory, Oxford
de Roever W-P, Engelhardt K (1998) Data refinement: model-oriented proof methods and their comparison. CUP, London
Bolton C, Davies J, Woodcock JCP On the refinement and simulation of data types and processes. In Araki et al. [9], pp 273–292
Deutsch M, Henson MC (2006) An analysis of refinement in an abortive paradigm. Form Asp Comput 18(3):329–363
Josephs MB (1988) A state-based approach to communicating processes. Distrib Comput 3:9–18
Boiten EA, de Roever W-P (2003) Getting to the bottom of relational refinement: relations and correctness, partial and total. In: Berghammer R, Möller B (eds) 7th International seminar on relational methods in computer science (RelMiCS 7). University of Kiel, Kiel, pp 82–88
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
Copyright information
© 2018 Springer International Publishing AG, part of Springer Nature
About this chapter
Cite this chapter
Derrick, J., Boiten, E. (2018). A Relational View of Refinement. In: Refinement. Springer, Cham. https://doi.org/10.1007/978-3-319-92711-4_4
Download citation
DOI: https://doi.org/10.1007/978-3-319-92711-4_4
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-92709-1
Online ISBN: 978-3-319-92711-4
eBook Packages: Computer ScienceComputer Science (R0)