Abstract
The end of the 1980s saw a growing interest in object orientation as both a design and programming methodology with the advent of programming languages like C++ and Eiffel. The trend was taken up by some in the formal methods community, including a team of researchers in Australia. Their contribution was a formal specification language, Object-Z, which had immediate industrial impact, gained rapid international recognition, and then two decades later began to fade, along with some of its contemporaries, from the formal methods scene. This paper details the rise and fall of Object-Z from the perspective of two of its original developers.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
The VDM series of conferences, of which VDM ’90 was a part, transformed into the FME series (in 1993) and later (in 2005) the current FM conference series.
References
Abrial, J.R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, New York (1996)
Abrial, J.R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, New York (2010)
Abrial, J.R., Schuman, S., Meyer, B.: Specification language. In: McKeag, R., Macnaghten, A. (eds.) On the Construction of Programs: An Advanced Course. Cambridge University Press, New York (1980)
Alencar, A.J., Goguen, J.A.: OOZE: an object oriented Z environment. In: America, P. (ed.) ECOOP 1991. LNCS, vol. 512, pp. 180–199. Springer, Heidelberg (1991). https://doi.org/10.1007/BFb0057022
Amálio, N., Polack, F.: Comparison of formalisation approaches of UML class constructs in Z and Object-Z. In: Bert, D., Bowen, J.P., King, S., Waldén, M. (eds.) ZB 2003. LNCS, vol. 2651, pp. 339–358. Springer, Heidelberg (2003). https://doi.org/10.1007/3-540-44880-2_21
America, P.: Issues in the design of a parallel object-oriented language. Formal Aspects Comput. 1(4), 366–411 (1989)
Bailes, C., Duke, R.: The ecology of class refinement. In: Morris, J.M., Shaw, R.C. (eds.) 4th Refinement Workshop, pp. 185–196. Springer, London (1991). https://doi.org/10.1007/978-1-4471-3756-6_10
Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: an overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 49–69. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-30569-9_3
Bear, S.: Structuring for the VDM specification language. In: Bloomfield, R.E., Marshall, L.S., Jones, R.B. (eds.) VDM 1988. LNCS, vol. 328, pp. 2–25. Springer, Heidelberg (1988). https://doi.org/10.1007/3-540-50214-9_2
Belina, F., Hogrefe, D.: The CCITT-specification and description language SDL. Comput. Netw. ISDN Syst. 16(4), 311–341 (1989)
Bergstra, J., Klop, J.: Process algebra for synchronous communication. Inf. Control 60, 109–137 (1984)
Birtwistle, G., Dahl, O.J., Myhrhaug, B., Nygaard, K.: Simula Begin. Auerbach, Philadelphia (1973)
Bobrow, D., Stefik, M.: LOOPS: an Object-Oriented Programming System for Interlisp. Technical report, Xerox PARC (1982)
Bolognesi, T., Brinksma, E.: Introduction to the ISO specification language LOTOS. Comput. Netw. ISDN Syst. 14, 25–59 (1987)
Bowen, J.P., Reeves, S.: From a community of practice to a body of knowledge: a case study of the formal methods community. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 308–322. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-21437-0_24
Brinksma, E., Scollo, G., Steenbergen, C.: LOTOS specifications, their implementations and their tests. In: Sarikaya, B., von Bochmann, G. (eds.) Protocol Specification, Testing, and Verification, VI. North-Holland (1987)
Burdy, L., et al.: An overview of JML tools and applications. Int. J. Softw. Tools Technol. Transf. (STTT) 7(3), 212–232 (2005)
Burstall, R., Goguen, J.: An informal introduction to specifications using Clear. In: Boyer, R., Moore, J. (eds.) The Correctness Problem in Computer Science, chap. 4. International Lecture Series in Computer Science. Academic Press (1981)
Cannon, H.: Flavors. Technical report, MIT Artificial Intelligence Laboratory (1980)
Carrington, D., et al.: Object-Z: an object-oriented extension to Z. In: Vuong, S. (ed.) Formal Description Techniques, II (FORTE 1989), pp. 281–296. North-Holland (1989)
Cox, B.: Object-Oriented Programming: An Evolutionary Approach. Addison-Wesley, Reading (1986)
Cusack, E.: Inheritance in object oriented Z. In: America, P. (ed.) ECOOP 1991. LNCS, vol. 512, pp. 167–179. Springer, Heidelberg (1991). https://doi.org/10.1007/BFb0057021
Derrick, J., Boiten, E.: Refinement in Z and Object-Z. Foundations and Advanced Applications. Springer, London (2001)
Derrick, J., Boiten, E., Bowman, H., Steen, M.: Translating LOTOS to Object-Z. In: 2nd BCS-FACS Northern Formal Methods Workshop. Workshops in Computing. Springer (1997)
Dong, J.S., Duke, R., Rose, G.: An object-oriented denotational semantics of a small programming language. Object Oriented Syst. 4, 29–52 (1997)
Dong, J.S., Duke, R.: The geometry of object containment. Object-Oriented Syst. 2(1), 41–63 (1995)
Duce, D.A., Duke, D.J., ten Hagen, P.J.W., Herman, I., Reynolds, G.J.: Formal methods in the development of PREMO. Comput. Stand. Interf. 17(5–6), 491–509 (1995)
Duke, D., Duke, R.: Towards a semantics for Object-Z. In: Bjørner, D., Hoare, C.A.R., Langmaack, H. (eds.) VDM 1990. LNCS, vol. 428, pp. 244–261. Springer, Heidelberg (1990). https://doi.org/10.1007/3-540-52513-0_14
Duke, R., Hayes, I.J., King, P., Rose, G.: Protocol specification and verification using Z. In: Aggarwal, S., Sabnani, K. (eds.) Protocol Specification, Testing, and Verification, VIII, pp. 33–46. North-Holland (1988)
Duke, R., King, P., Rose, G., Smith, G.: The Object-Z specification language. In: Korson, T., Vaishnavi, V., Meyer, B. (eds.) Technology of Object-Oriented Languages and Systems: TOOLS 5, pp. 465–483. Prentice Hall International (1991)
Duke, R., Rose, G.: Specifying a sliding-window protocol. In: Proceedings 11th Australian Computer Science Conference (ACSC-11), pp. 352–361. Australian Computer Science Association (1988)
Duke, R., Rose, G.: Formal Object-Oriented Specification Using Object-Z. Macmillan, Basingstoke (2000)
Duke, R., Rose, G., Smith, G.: Transferring formal techniques to industry: a case study. In: Formal Description Techniques (FORTE 1990), pp. 279–286. North-Holland (1990)
Duke, R., Rose, G., Smith, G.: Object-Z: a specification language advocated for the description of standards. Comput. Stand. Interf. 17(5–6), 511–533 (1995)
Duke, R., Smith, G.: Temporal logic and Z specifications. In: Proceedings 12th Australian Computer Science Conference (ACSC-12), Appendix, pp. 32–42. Australian Computer Science Association (1989)
Fischer, C.: CSP-OZ - a combination of CSP and Object-Z. In: Bowman, H., Derrick, J. (eds.) Formal Methods for Open Object-Based Distributed Systems (FMOODS 1997), pp. 423–438. Chapman & Hall (1997)
Goguen, J., Meseguer, J.: Unifying functional, object-oriented, and relational programming with logical semantics. In: Shriver, B., Wegner, P. (eds.) Research Directions in Object-Oriented Programming, pp. 417–477. MIT Press (1987)
Goguen, J., Tardo, J.: An introduction to OBJ: a language for writing and testing software specifications. In: Gehani, N., McGettrick, A. (eds.) Software Specification Techniques, pp. 391–420. Addison-Wesley (1985)
Goldberg, A., Robson, D.: Smalltalk 80: The Language and its Implementation. Addison-Wesley, Reading (1983)
Griffiths, A.: From Object-Z to Eiffel: a rigorous development method. In: Mingins, C., Duke, R., Meyer, B. (eds.) Technology of Object-Oriented Languages and Systems (TOOLS 18), pp. 293–308. Prentice Hall (1995)
Griffiths, A.: An extended semantic foundation for Object-Z. In: 1996 Asia-Pacific Software Engineering Conference (APSEC 1996), pp. 194–207. IEEE Computer Society Press (1996)
Hall, A.: Using Z as a specification calculus for object-oriented systems. In: Bjørner, D., Hoare, C.A.R., Langmaack, H. (eds.) VDM 1990. LNCS, vol. 428, pp. 290–318. Springer, Heidelberg (1990). https://doi.org/10.1007/3-540-52513-0_16
Hayes, I.J.: Applying formal specification to software development in industry. IEEE Trans. Softw. Eng. SE 11(2), 169–178 (1985)
Hayes, I.J., Mowbray, M., Rose, G.: Signalling System No. 7: the network layer. In: Aggarwal, S., Sabnani, K. (eds.) Protocol Specification, Testing, and Verification, IX. North-Holland (1989)
Hayes, I.J. (ed.): Specification Case Studies. Series in Computer Science, 2nd edn. Prentice Hall International, London (1993)
Hoare, C.A.R.: Communicating Sequential Processes. Series in Computer Science. Prentice Hall International, London (1985)
Hoare, T.: The verifying compiler: a grand challenge for computing research. In: Böszörményi, L., Schojer, P. (eds.) JMLC 2003. LNCS, vol. 2789, pp. 25–35. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-45213-3_4
Hoare, C.A.R., He, J.: Unifying Theories of Programming. Series in Computer Science. Prentice Hall International, Englewood Cliffs (1998)
ISO TC97/SC21: Estelle - A Formal Description Technique Based on an Extended State Transition Model (1988). International Standard 9074
ISO/IEC 13568:2002: Information Technology - Z Formal Specification Notation- Syntax, Type System and Semantics (2002)
Jackson, D.: Software Abstractions - Logic, Language, and Analysis. MIT Press, Cambridge (2006). Revised 2011
Johnston, W.: A Type Checker for Object-Z. Technical report 96–24, Software Verification Research Centre, The University of Queensland (1996)
Johnston, W., Rose, G.: Guidelines for the Manual Conversion of Object-Z to C++. Technical report 93–14, Software Verification Research Centre, The University of Queensland (1993)
Jones, C.: Systematic Software Development Using VDM. Series in Computer Science. Prentice Hall International, Englewood Cliffs (1986)
Kassel, G., Smith, G.: Model checking Object-Z classes: some experiments with FDR. In: 8th Asia-Pacific Software Engineering Conference (APSEC 2001), pp. 445–452. IEEE Computer Society Press (2001)
Kim, S.-K., David, C.: Formalizing the UML class diagram using Object-Z. In: France, R., Rumpe, B. (eds.) UML 1999. LNCS, vol. 1723, pp. 83–98. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-46852-8_7
Kim, S.-K., Carrington, D.: A formal mapping between UML models and Object-Z specifications. In: Bowen, J.P., Dunne, S., Galloway, A., King, S. (eds.) ZB 2000. LNCS, vol. 1878, pp. 2–21. Springer, Heidelberg (2000). https://doi.org/10.1007/3-540-44525-0_2
King, P.: Printing Z and Object-Z LaTeX Documents (1990)
Lano, K.: Z++, an object-orientated extension to Z. In: Nicholls, J. (ed.) Z User Workshop, Oxford 1990. Workshops in Computing. Springer, London (1990). https://doi.org/10.1007/978-1-4471-3540-1_11
Lano, K., Haughton, H.: Object-Oriented Specification Case Studies. Prentice Hall International, New York (1994)
Lave, J., Wenger, E.: Situated Learning: Legitimate Peripheral Participation. Cambridge University Press, Cambridge (1991)
Malik, P., Utting, M.: CZT: a framework for Z tools. In: Treharne, H., King, S., Henson, M., Schneider, S. (eds.) ZB 2005. LNCS, vol. 3455, pp. 65–84. Springer, Heidelberg (2005). https://doi.org/10.1007/11415787_5
Mayr, T.: Specification of object-oriented systems in LOTOS. In: Turner, K. (ed.) Formal Description Techniques (FORTE 1988), pp. 107–119. North-Holland (1988)
McComb, T., Smith, G.: A minimal set of refactoring rules for Object-Z. In: Barthe, G., de Boer, F.S. (eds.) FMOODS 2008. LNCS, vol. 5051, pp. 170–184. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-68863-1_11
Meira, S., Cavalcanti, A.: Modular object-oriented Z specifications. In: Nicholls, J. (ed.) Z User Workshop, Oxford 1990. Workshops in Computing. Springer, London (1990). https://doi.org/10.1007/978-1-4471-3540-1_12
Meyer, B.: Object-Oriented Software Construction. Series in Computer Science. Prentice Hall International, Englewood Cliffs (1988)
Miao, H., Liu, L., Li, L.: Formalizing UML models with Object-Z. In: George, C., Miao, H. (eds.) ICFEM 2002. LNCS, vol. 2495, pp. 523–534. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-36103-0_53
Milner, R.: Communication and Concurrency. Prentice Hall, Upper Saddle River (1989)
Narfelt, K.: SYSDAX - an object oriented design methodology based on SDL. In: SDL 1987: State of the Art and Future Trends. North-Holland (1987)
Nielsen, M., Havelund, K., Wagner, K.R., George, C.: The RAISE language, method and tools. In: Bloomfield, R.E., Marshall, L.S., Jones, R.B. (eds.) VDM 1988. LNCS, vol. 328, pp. 376–405. Springer, Heidelberg (1988). https://doi.org/10.1007/3-540-50214-9_25
Roe, D., Broda, K., Russo, A.: Mapping UML models incorporating OCL constraints into Object-Z. Technical report, Department of Computing, Imperial College London (2003)
Rose, G., Duke, R., Hayes, I.J.: Specifying communications services and protocols. In: Proceedings 2nd Australian Software Engineering Conference (ASWEC 1987), pp. 161–170. The Institution of Radio and Electronics Engineers Australia (1987)
Rosenberg, K.: The adoption of formal methods within OTC. In: Parker, K., Rose, G. (eds.) Formal Description Techniques, IV (FORTE 1991), pp. 91–98. Elsevier (1992)
Schuman, S., Pitt, D.: Object-oriented subsystem specification. In: Meertens, L. (ed.) Program Specification and Transformation, pp. 313–341. North-Holland (1987)
Sijelmassi, R., Gaudette, P.: An object-oriented model for Estelle. In: Turner, K. (ed.) Formal Description Techniques (FORTE 1988), pp. 91–105. North-Holland (1988)
Smith, G.: A formal specification of Signalling System No. 7 Telephone User Part. In: Proceedings 1989 Singapore International Conference on Networks (SICON 1989), pp. 50–55. IEEE Singapore Section (1989)
Smith, G.: A semantic integration of Object-Z and CSP for the specification of concurrent systems. In: Fitzgerald, J., Jones, C.B., Lucas, P. (eds.) FME 1997. LNCS, vol. 1313, pp. 62–81. Springer, Heidelberg (1997). https://doi.org/10.1007/3-540-63533-5_4
Smith, G.: The Object-Z Specification Language. Advances in Formal Methods Series. Kluwer Academic Publishers (2000)
Smith, G.: Introducing reference semantics via refinement. In: George, C., Miao, H. (eds.) ICFEM 2002. LNCS, vol. 2495, pp. 588–599. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-36103-0_60
Smith, G., Duke, R.: Modelling a cache coherence protocol using Object-Z. In: Proceedings 13th Australian Computer Science Conference (ACSC-13), pp. 352–361. Australian Computer Science Association (1990)
Smith, G., Kammüller, F., Santen, T.: Encoding Object-Z in Isabelle/HOL. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds.) ZB 2002. LNCS, vol. 2272, pp. 82–99. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45648-1_5
Spivey, J.M.: Understanding Z: A Specification Language and its Formal Semantics, Cambridge Tracts in Theoretical Computer Science, vol. 3. Cambridge University Press, Cambridge (1988)
Spivey, J.M.: The Z Notation: A Reference Manual. Series in Computer Science, Prentice Hall International, Englewood Cliffs (1989). 2nd edn. 1992
Stepney, S., Barden, R., Cooper, D.: Object Orientation in Z. Workshops in Computing. Springer, London (1992). https://doi.org/10.1007/978-1-4471-3552-4
Stepney, S., Barden, R., Cooper, D.: A survey of object orientation in Z. Softw. Eng. J. 7(2), 150–160 (1992)
Stroustrup, B.: The C++ Programming Language. Addison-Wesley, Boston (1986)
Treharne, H., Schneider, S.: Using a process algebra to control B operations. In: Araki, K., Galloway, A., Taguchi, K. (eds.) IFM 1999, vol. 1945, pp. 437–456. Springer, London (1999). https://doi.org/10.1007/978-1-4471-0851-1_23
Whysall, P., McDermid, J.: An approach to object oriented specification using Z. In: Nicholls, J. (ed.) Z User Workshop, Oxford 1990. Workshops in Computing. Springer, London (1990). https://doi.org/10.1007/978-1-4471-3540-1_13
Wills, A.: Capsules and types in Fresco. In: America, P. (ed.) ECOOP 1991. LNCS, vol. 512, pp. 59–76. Springer, Heidelberg (1991). https://doi.org/10.1007/BFb0057015
Woodcock, J., Cavalcanti, A.: The semantics of Circus. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds.) ZB 2002. LNCS, vol. 2272, pp. 184–203. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45648-1_10
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2020 Springer Nature Switzerland AG
About this paper
Cite this paper
Smith, G., Duke, D.J. (2020). Specification with Class: A Brief History of Object-Z. In: Sekerinski, E., et al. Formal Methods. FM 2019 International Workshops. FM 2019. Lecture Notes in Computer Science(), vol 12233. Springer, Cham. https://doi.org/10.1007/978-3-030-54997-8_4
Download citation
DOI: https://doi.org/10.1007/978-3-030-54997-8_4
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-54996-1
Online ISBN: 978-3-030-54997-8
eBook Packages: Computer ScienceComputer Science (R0)