Abstract
This chapter concludes the discussion on more liberal forms of Z refinement, by discussing a few more options, and how they all fit together. It looks at whether new operations can be added without relating to any previous operations, or as multiple copies of previous ones: alphabet extension, and alphabet translation. It also describes a generalisation which looks at approximate refinement between abstract and concrete systems.
Excerpts from pp. 159–160 of [8] are reprinted within Sect. 14.1 with kind permission of Springer Science and Business Media.
Excerpts from pp. 377–381 of [9] are reprinted within Sect. 14.4 with kind permission of Springer Science and Business Media.
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.
The standard semantics of applying Remove outside its precondition allows for any result including the “correct” one and a completely undefined one; however, we are looking for equality of semantics of programs rather than the inclusion.
References
Abrial, J.-R. (2010). Modelling in Event-B. Cambridge: Cambridge University Press.
Banach, R., Jeske, C., Poppleton, M., & Stepney, S. (2007). Retrenching the purse: the balance enquiry quandary, and generalised and (1, 1) forward refinements. Fundamenta Informaticae, 77(1–2), 29–69.
Banach, R., & Poppleton, M. (2000) Retrenchment, refinement and simulation. In Bowen et al. [10] (pp. 304–323).
Banach, R., Poppleton, M., Jeske, C., & Stepney, S. (2005) Retrenching the purse: Finite sequence numbers, and the tower pattern. In Fitzgerald et al. [12] (pp. 382–398).
Banach, R., Poppleton, M., Jeske, C., & Stepney, S. (2006). Retrenching the purse: hashing injective CLEAR codes, and security properties. In Leveraging Applications of Formal Methods, Second International Symposium, ISoLA, Cyprus (pp. 82–90). New York: IEEE Press.
Banach, R., Poppleton, M., & Stepney, S. (2006). Retrenching the purse: finite exception logs, and validating the small. In 30th Annual IEEE/NASA Software Engineering Workshop (SEW-30) (pp. 234–248). Los Alamitos: IEEE Comput. Soc.
Boiten, E. A. (2012). Introducing extra operations in refinement. Formal Aspects of Computing. doi:10.1007/s00165-012-0266-z.
Boiten, E. A., & Derrick, J. (2000). Liberating data refinement. In R. C. Backhouse & J. N. Oliveira (Eds.), Mathematics of Program Construction. Lecture Notes in Computer Science: Vol. 1837 (pp. 144–166). Berlin: Springer.
Boiten, E. A., & Derrick, J. (2005) Formal program development with approximations. In Treharne et al. [19] (pp. 374–392).
Bowen, J. P., Dunne, S., Galloway, A., & King, S. (Eds.) (2000). ZB2000: Formal Specification and Development in Z and B. Lecture Notes in Computer Science: Vol. 1878. Berlin: Springer.
de Bakker, J. W., & Meyer, J.-J. C. (1992). Metric semantics for concurrency. In J. W. de Bakker & J. J. M. Rutten (Eds.), Ten Years of Concurrency Semantics: Selected Papers of the Amsterdam Concurrency Group (pp. 104–130). Singapore: World Scientific.
Fitzgerald, J. A., Hayes, I. J., & Tarlecki, A. (Eds.) (2005). FM 2005: Formal Methods, International Symposium of Formal Methods Europe. Lecture Notes in Computer Science: Vol. 3582. Berlin: Springer.
Groves, L. (2002). Refinement and the Z schema calculus. Electronic Notes in Theoretical Computer Science, 70(3), 70–93.
Groves, L. (2005) Practical data refinement for the Z schema calculus. In Treharne et al. [19] (pp. 393–413).
Helke, S., & Santen, T. (2001). Mechanized analysis of behavioral conformance in the Eiffel base libraries. In J. N. Oliveira & P. Zave (Eds.), FME’01—International Symposium of Formal Methods Europe. Lecture Notes in Computer Science: Vol. 2021 (pp. 20–42). Berlin: Springer.
Liskov, B., & Wing, J. M. (1994). A behavioural notion of subtyping. ACM Transactions on Programming Languages and Systems, 16(6), 1811–1841.
Neilson, D. S. (1990). From Z to C: illustration of a rigorous development method. PhD thesis, Oxford University Computing Laboratory.
Smith, G. (1999). From ideal to realisable real-time specifications. In N. Leslie (Ed.), Fifth New Zealand Formal Program Development Colloquium. Number 99-1 in IIMS Technical Report. Institute of Information and Mathematical Sciences, Massey University at Albany.
Treharne, H., King, S., Henson, M. C., & Schneider, S. A. (Eds.) (2005). ZB 2005: Formal Specification and Development in Z and B, 4th International Conference of B and Z Users. Lecture Notes in Computer Science: Vol. 3455. Berlin: Springer.
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). Further Generalisations. In: Refinement in Z and Object-Z. Springer, London. https://doi.org/10.1007/978-1-4471-5355-9_14
Download citation
DOI: https://doi.org/10.1007/978-1-4471-5355-9_14
Publisher Name: Springer, London
Print ISBN: 978-1-4471-5354-2
Online ISBN: 978-1-4471-5355-9
eBook Packages: Computer ScienceComputer Science (R0)