Abstract
In this chapter we adapt the refinement rules derived for Z to Object-Z specifications consisting of just a single class, taking into account the consequences of the different interpretation of preconditions. We also consider how weak refinement and non-atomic refinement may be applied to Object-Z. Finally, we discuss the relation between refinement, and two other important concepts in object orientation: subtyping and inheritance.
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.
There is an implicit fairness assumption in the formulation of weak refinement in that if an internal operation is enabled then it is assumed that it will eventually occur. This is the same assumption underlying the use of internal events in many process algebras.
- 2.
Failing to use renaming here would identify all four digits, limiting the specification to a very commonly used and thus very insecure subset of pin codes.
References
America, P. (1990). A parallel object-oriented language with inheritance and subtyping. In Proceedings of the OOPSLA/ECOOP ’90 Conference on Object-Oriented Programming Systems, Languages and Applications (pp. 161–168). Published as ACM SIGPLAN Notices, volume 25, number 10.
Back, R. J. R., & von Wright, J. (1994). Trace refinement of action systems. In B. Jonsson & J. Parrow (Eds.), CONCUR’94: Concurrency Theory, Uppsala, Sweden, August 1994. Lecture Notes in Computer Science: Vol. 836 (pp. 367–384). Berlin: Springer.
Bolton, C., & Davies, J. (2002). Refinement in Object-Z and CSP. In M. Butler, L. Petre, & K. Sere (Eds.), Integrated Formal Methods (IFM 2002). Lecture Notes in Computer Science: Vol. 2335 (pp. 225–244). Berlin: Springer.
Bonsangue, M., Kok, J., & Sere, K. (1999) Developing object-based distributed systems. In Ciancarini et al. [7] (pp. 19–34).
Bowen, J. P. & Hinchey, M. G. (Eds.) (1995). ZUM’95: the Z Formal Specification Notation. Lecture Notes in Computer Science: Vol. 967. Limerick: Springer.
Canver, E., & von Henke, F. W. (1999) Formal development of object-based systems in a temporal logic setting. In Ciancarini et al. [7] (pp. 419–436).
Ciancarini, P., Fantechi, A., & Gorrieri, R. (Eds.) (1999). Formal Methods for Open Object-Based Distributed Systems. Dordrecht: Kluwer Academic.
Cusack, E. (1991). Inheritance in object oriented Z. In P. America (Ed.), ECOOP ’91—Object-Oriented Programming. Lecture Notes in Computer Science: Vol. 512 (pp. 167–179). Berlin: Springer.
Derrick, J., & Wehrheim, H. (2003). Using coupled simulations in non-atomic refinement. In D. Bert, J. P. Bowen, S. King, & M. Waldén (Eds.), ZB 2003: Formal Specification and Development in Z and B. Lecture Notes in Computer Science: Vol. 2651 (pp. 127–147). Berlin: Springer.
Duke, R., Bailes, C., & Smith, G. (1996). A blocking model for reactive objects. Formal Aspects of Computing, 8(3), 347–368.
Fischer, C., & Wehrheim, H. (2000). Behavioural subtyping relations for object-oriented formalisms. In T. Rus (Ed.), Algebraic Methodology and Software Technology. Lecture Notes in Computer Science: Vol. 1816 (pp. 469–483). Berlin: Springer.
Fitzgerald, J. A., Jones, C. B., & Lucas, P. (Eds.) (1997). FME’97: Industrial Application and Strengthened Foundations of Formal Methods. Lecture Notes in Computer Science: Vol. 1313. Berlin: Springer.
Hinchey, M. G. & Liu, S. (Eds.) (1997). First International Conference on Formal Engineering Methods (ICFEM’97). Hiroshima, Japan, November 1997. Los Alamitos: IEEE Comput. Soc.
Järvinen, H. M., & Kurki-Suonio, R. (1991). DisCo specification language: marriage of actions and objects. In 11th International Conference on Distributed Computing Systems, Washington, DC, USA, May 1991 (pp. 142–151). Los Alamitos: IEEE Comput. Soc.
Lamport, L. (1994). The temporal logic of actions. ACM Transactions on Programming Languages and Systems, 16(3), 872–923.
Liskov, B., & Wing, J. M. (1995) Specifications and their use in defining subtypes. In Bowen and Hinchey [5] (pp. 245–263).
Smith, G. (1995). A fully abstract semantics of classes for Object-Z. Formal Aspects of Computing, 7(3), 289–313.
Smith, G. (1997) A semantic integration of Object-Z and CSP for the specification of concurrent systems. In Fitzgerald et al. [12] (pp. 62–81).
Smith, G., & Derrick, J. (1997) Refinement and verification of concurrent systems specified in Object-Z and CSP. In Hinchey and Liu [13] (pp. 293–302).
Strulo, B. (1995) How firing conditions help inheritance. In Bowen and Hinchey [5] (pp. 264–275).
Wehrheim, H. (2000). Behavioural subtyping and property preservation. In S. F. Smith & C. L. Talcott (Eds.), Formal Methods for Open Object-Based Distributed Systems (FMOODS 2000) (pp. 213–231). Dordrecht: Kluwer Academic.
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). Refinement in Object-Z. In: Refinement in Z and Object-Z. Springer, London. https://doi.org/10.1007/978-1-4471-5355-9_16
Download citation
DOI: https://doi.org/10.1007/978-1-4471-5355-9_16
Publisher Name: Springer, London
Print ISBN: 978-1-4471-5354-2
Online ISBN: 978-1-4471-5355-9
eBook Packages: Computer ScienceComputer Science (R0)