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.


Internal Operation Abstract Operation Bibliographical Note Concrete Operation Refinement Methodology 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  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