×

An institution for Object-Z with inheritance and polymorphism. (English) Zbl 1453.68043

De Nicola, Rocco (ed.) et al., Software, services, and systems. Essays dedicated to Martin Wirsing on the occasion of his retirement from the chair of programming and software engineering, Munich, Germany, 2015. Essays. Cham: Springer. Lect. Notes Comput. Sci. 8950, 134-154 (2015).
Summary: Large software systems are best specified using a multi-paradigm approach. Depending on which aspects of a system one wants to model, some logic formalisms are better suited than others. The theory of institutions and (co)morphisms between institutions provides a general framework for describing logical systems and their connections. This is the foundation of multi-modelling languages allowing one to deal with heterogeneous specifications in a consistent way. To make Object-Z accessible as part of such a multi-modelling language, we define the institution OZS for Object-Z. We have chosen Object-Z in part because it is a prominent software modelling language and in part because it allows us to study the formalisation of object-oriented concepts, like object identity, object state, dynamic behaviour, polymorphic sorts and inheritance.
For the entire collection see [Zbl 1312.68005].

MSC:

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q65 Abstract data types; algebraic specification

Software:

CASL; Hets; Z
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Rumbaugh, J., Jacobson, I., Booch, G.: The Unified Modeling Language. Reference Manual, 2nd edn. Addison-Wesley Professional (2004)
[2] Mossakowski, T., Maeder, C., Codescu, M.: Hets user guide - verion 0.99. DKFI GmbH, Bremen, Germany (2013)
[3] Mossakowski, T.: Heterogeneous specification and the heterogeneous tool set. Habilitation thesis, University of Bremen (2005)
[4] Goguen, J.A., Burstall, R.M.: Introducing institutions. In: Clarke, E., Kozen, D. (eds.) Logic of Programs 1983. LNCS, vol. 164, pp. 221–256. Springer, Heidelberg (1984) · Zbl 0543.68021 · doi:10.1007/3-540-12896-4_366
[5] Burstall, R.M., Goguen, J.A.: The semantics of Clear, a specification language. In: Bjorner, D. (ed.) Abstract Software Specifications. LNCS, vol. 86, pp. 292–332. Springer, Heidelberg (1980) · Zbl 0456.68024 · doi:10.1007/3-540-10007-5_41
[6] Sannella, D., Tarlecki, A.: Specifications in an arbitrary institution. Information and Computation (1988) · Zbl 0654.68017 · doi:10.1016/0890-5401(88)90008-9
[7] Mosses, P.D. (ed.): CASL Reference Manual. LNCS, vol. 2960. Springer, Heidelberg (2004) · Zbl 1046.68001
[8] Ehrig, H., Mahr, B.: Fundamentals of algebraic specification 1: Equations and initial semantics. Springer (1985) · Zbl 0557.68013 · doi:10.1007/978-3-642-69962-7
[9] Smith, D.R.: Composition by colimit and formal software development. In: Futatsugi, K., Jouannaud, J.-P., Meseguer, J. (eds.) Algebra, Meaning, and Computation. LNCS, vol. 4060, pp. 317–332. Springer, Heidelberg (2006) · Zbl 1132.68341 · doi:10.1007/11780274_17
[10] Smith, G.: The Object-Z specification language. Kluwer Academic Publisher (2000) · Zbl 0944.68124 · doi:10.1007/978-1-4615-5265-9
[11] Spivey, J.M.: The Z Notation - A Reference manual. Prentice-Hall (1989) · Zbl 0777.68003
[12] 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.) B 2000, ZUM 2000, and ZB 2000. LNCS, vol. 1878, pp. 2–21. Springer, Heidelberg (2000) · doi:10.1007/3-540-44525-0_2
[13] Baumeister, H.: Relating abstract datatypes and Z-schemata. In: Bert, D., Choppy, C., Mosses, P.D. (eds.) WADT 1999. LNCS, vol. 1827, pp. 366–382. Springer, Heidelberg (2000) · Zbl 0966.68134 · doi:10.1007/978-3-540-44616-3_21
[14] Cengarle, M.V., Knapp, A.: An institution for UML 2.0 static structures. Technical Report TUM-10807, Technische Universität München (2008)
[15] Cengarle, M.V., Knapp, A., Tarlecki, A., Wirsing, M.: A heterogeneous approach to UML semantics. In: Degano, P., De Nicola, R., Meseguer, J. (eds.) Concurrency, Graphs and Models. LNCS, vol. 5065, pp. 383–402. Springer, Heidelberg (2008) · Zbl 1143.68373 · doi:10.1007/978-3-540-68679-8_23
[16] Boronat, A., Knapp, A., Meseguer, J., Wirsing, M.: What is a multi-modeling language? In: Corradini, A., Montanari, U. (eds.) WADT 2008. LNCS, vol. 5486, pp. 71–87. Springer, Heidelberg (2009) · Zbl 1253.68225 · doi:10.1007/978-3-642-03429-9_6
[17] Baumeister, H.: Relations between Abstract Datatypes modeled as Abstract Datatypes. PhD thesis, University of Saarbrücken (1999)
[18] Goguen, J.A., Meseguer, J.: Order-sorted algebra I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations. Theoretical Computer Science 105(2), 217–273 (1992) · Zbl 0778.68056 · doi:10.1016/0304-3975(92)90302-V
[19] Meseguer, J.: Membership algebra as a logical framework for equational specification. In: Parisi-Presicce, F. (ed.) WADT 1997. LNCS, vol. 1376, pp. 18–61. Springer, Heidelberg (1998) · Zbl 0903.08009 · doi:10.1007/3-540-64299-4_26
[20] Goguen, J.A., Burstall, R.M.: Institutions: Abstract model theory for specification and programming. Journal of the ACM (JACM) 39(1), 95–146 (1992) · Zbl 0799.68134 · doi:10.1145/147508.147524
[21] Somerville, I.: Model-based specification (2000), http://www.cs.st-andrews.ac.uk/ ifs/Resources/Notes/FormalSpec/ModelSpec.pdf
[22] Baumeister, H., Bettaz, M., Maouche, M., Mosteghanemi, M.: Institutions for Object-Z – technical report (2014), http://people.compute.dtu.dk/huba/publications/OZReport.pdf · Zbl 1453.68043
[23] Mac Lane, S.: Categories for the working mathematician, 2nd edn., vol. 5. Springer (1998) · Zbl 0906.18001
[24] Wen, Z., Miao, H., Zeng, H.: Generating proof obligation to verify Object-Z specification. In: IEEE International Conference on Software Engineering Advances, pp. 38–38 (2006) · doi:10.1109/ICSEA.2006.261294
[25] Stevens, B.: Implementing Object-Z with Perfect Developer. Journal of Object Technology 5(2), 189–202 (2006) · Zbl 05431400 · doi:10.5381/jot.2006.5.2.a5
[26] Paige, R.F., Brooke, P.J.: Integrating BON and Object-Z. Journal of Object Technology 3(3), 121–141 (2004) · Zbl 05431344 · doi:10.5381/jot.2004.3.3.a3
[27] Codescu, M., Horozal, F., Jakubauskas, A., Mossakowski, T., Rabe, F.: Compiling logics. In: Martí-Oliet, N., Palomino, M. (eds.) WADT 2012. LNCS, vol. 7841, pp. 111–126. Springer, Heidelberg (2013) · Zbl 1394.68071 · doi:10.1007/978-3-642-37635-1_7
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.