Refinement in Object-Z

  • John Derrick
  • Eerke A. Boiten


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.




  1. 1.
    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. Google Scholar
  2. 2.
    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. Google Scholar
  3. 3.
    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. CrossRefGoogle Scholar
  4. 4.
    Bonsangue, M., Kok, J., & Sere, K. (1999) Developing object-based distributed systems. In Ciancarini et al. [7] (pp. 19–34). Google Scholar
  5. 5.
    Bowen, J. P. & Hinchey, M. G. (Eds.) (1995). ZUM’95: the Z Formal Specification Notation. Lecture Notes in Computer Science: Vol. 967. Limerick: Springer. MATHGoogle Scholar
  6. 6.
    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). Google Scholar
  7. 7.
    Ciancarini, P., Fantechi, A., & Gorrieri, R. (Eds.) (1999). Formal Methods for Open Object-Based Distributed Systems. Dordrecht: Kluwer Academic. MATHGoogle Scholar
  8. 8.
    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. Google Scholar
  9. 9.
    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. CrossRefGoogle Scholar
  10. 10.
    Duke, R., Bailes, C., & Smith, G. (1996). A blocking model for reactive objects. Formal Aspects of Computing, 8(3), 347–368. MATHCrossRefGoogle Scholar
  11. 11.
    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. CrossRefGoogle Scholar
  12. 12.
    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. Google Scholar
  13. 13.
    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. Google Scholar
  14. 14.
    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. Google Scholar
  15. 15.
    Lamport, L. (1994). The temporal logic of actions. ACM Transactions on Programming Languages and Systems, 16(3), 872–923. CrossRefGoogle Scholar
  16. 16.
    Liskov, B., & Wing, J. M. (1995) Specifications and their use in defining subtypes. In Bowen and Hinchey [5] (pp. 245–263). Google Scholar
  17. 17.
    Smith, G. (1995). A fully abstract semantics of classes for Object-Z. Formal Aspects of Computing, 7(3), 289–313. CrossRefGoogle Scholar
  18. 18.
    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). Google Scholar
  19. 19.
    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). Google Scholar
  20. 20.
    Strulo, B. (1995) How firing conditions help inheritance. In Bowen and Hinchey [5] (pp. 264–275). Google Scholar
  21. 21.
    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. Google Scholar

Copyright information

© Springer-Verlag London 2014

Authors and Affiliations

  • John Derrick
    • 1
  • Eerke A. Boiten
    • 2
  1. 1.Department of Computer ScienceUniversity of SheffieldSheffieldUK
  2. 2.School of ComputingUniversity of KentCanterburyUK

Personalised recommendations