×

zbMATH — the first resource for mathematics

Categorical foundations for structured specifications in \(\mathsf{Z}\). (English) Zbl 1385.68023
The paper uses the category-theoretic form of abstract model theory known as “institution theory” for providing foundations for the Z formal specification language. In particular this applies to the structuring mechanism of Z. Morever, the proposed foundations allow for heterogenous combinations of Z with other specification formalisms; this is illustrated with the combination of Z and CSP.

MSC:
68Q65 Abstract data types; algebraic specification
Software:
Circus; Eiffel; Hets; Z
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Baar T, Strohmeier A, Moreira A, Mellor S (2004) UML 2004. In: Lecture notes in computer science, vol 3273. Springer, Berlin
[2] Barr M, Wells C (1999) Category theory for computer science. In: Centre de Recherches Mathématiques, Université de Montréal · Zbl 0714.18001
[3] Baumeister H (1999) Relating abstract datatypes and Z-schemata. In: Proc. of WADT ’99. Lecture notes in computer science, vol 1827. Springer, Berlin, pp 366-382 · Zbl 0966.68134
[4] Bérnabou J (1967) Introduction to bicategories. In: Complementary definitions of programming language semantics. LNM vol 42. Springer, Berlin, pp 1-77
[5] Borzyszkowski T (1999) Higher-order logic and theorem proving for structured specifications. In: Proc. of WADT ’99. Lecture notes in computer science, vol 1827. Springer, Berlin · Zbl 0966.03010
[6] Brien, SM; Martin, AP, A calculus for schemas in Z, J Symb Comput, 30, 63-91, (2000) · Zbl 0962.68112
[7] Bujorianu MC (2004) Integration of specification languages using viewpoints. In: Proc. of IFM ’04. Lecture notes in computer science, vol 2999. Springer, Berlin · Zbl 1196.68128
[8] Castro PF, Aguirre N, Lopez Pombo CG, Maibaum TSE (2012) A categorical approach to structuring and promoting Z specifications. In: Proc. of FACS’12. Lecture notes in computer science, vol 7684. Springer, Berlin
[9] Chang CC, Keisler HJ (1990) Model theory. 3rd edn. North Holland, NY
[10] Diaconescu R (2008) Institution-independent model theory. Birkhäuser Verlag, Basel · Zbl 1144.03001
[11] Enderton H (2001) A mathematical introduction to logic. 2nd ed., Academic Press, Dublin · Zbl 0992.03001
[12] Fiadeiro J (2004) Categories for software engineering. Springer, Berlin · Zbl 1138.68365
[13] Fiadeiro, J; Maibaum, TSE, Temporal theories as modularisation units for concurrent system specification, Form Asp Comput, 4, 239-272, (1992) · Zbl 0746.68031
[14] Finkelstein, A; Kramer, J; Nuseibeh, B; Finkelstein, L; Goedicke, M, Viewpoints: a framework for integrating multiple perspectives in system development, Int J Softw Eng Knowl Eng, 2, 31-57, (1992)
[15] Fischer C (1997) Combining CSP and Z. Technical Report, University of Oldenburg
[16] Goguen, J; Burstall, R, Institutions: abstract model theory for specification and programming, J ACM, 39, 95-146, (1992) · Zbl 0799.68134
[17] Henson, M; Reeves, S, Revising Z: part I—logic and semantics, Form Asp Comput, 11, 359-380, (1999) · Zbl 0955.68077
[18] Henson, M; Reeves, S, Revising Z: part II—logical development, Form Asp Comput, 11, 381-401, (1999) · Zbl 0955.68078
[19] Hoare CAR, Jifeng H (1998) Unifying theories of programming. Prentice Hall College Division, Englewood Cliffs
[20] Jacky J (1997) The way of Z, practical programming with formal methods. Cambridge University Press, Cambridge
[21] Lano K (2009) Model-driven software development with UML and java. Course Technology · Zbl 0955.68078
[22] MacLane S (1998) Categories for the working mathematician. 2nd edn. Springer, Berlin · Zbl 0705.18001
[23] Meyer B (2000) Object-oriented software construction. Prentice Hall, Englewood Cliffs
[24] Mossakowski T, Maeder C, Lüttich K (2007) The heterogeneous tool set (hets). In: Proc. of 4th international verification workshop in connection with CADE-21. http://CEUR-WS.org · Zbl 0962.68112
[25] Nicholls J (1995) Z notation: version 1.2. Z standards panel
[26] Mossakowski T, Tarlecki A. Pawlowski W (1997) Combining and representing logical systems. In: Proc. of category theory and computer science’97. Lecture notes in computer science, vol 1290. Springer, Berlin · Zbl 0881.03044
[27] Mossakowski T, Roggenbach M (2006) Structured CSP—a process algebra as an institution. In: Proc. of WADT’06. Lecture notes in computer science, vol 4409. Springer, Berlin · Zbl 1196.68159
[28] Oliveira, M; Cavalcanti, A; Woodcock, J, A UTP semantics for circus, Form Asp Comput, 21, 3-32, (2009) · Zbl 1165.68048
[29] Parnas, D, On the criteria to be used in decomposing systems into modules, Commun. ACM, 15, 1053-1058, (1972)
[30] Parnas, D, The modular structure of complex system, IEEE Trans Softw Eng, 11, 259-266, (1985)
[31] Risk! Rules of Play (1963) Parker Brothers
[32] Spivey JM (1984) Towards a formal semantics for the Z notation. Oxford University Computing Laboratory, T.M. PRG-41
[33] Spivey JM (1988) Understanding Z: a specification language and its formal semantics. Cambridge Tracts in Theoretical Computer Science · Zbl 0658.68005
[34] Spivey JM (1992) The Z notation: a reference manual. Prentice Hall, Englewood Cliffs
[35] Tarlecki A (1995) Moving between logical systems. In: Proc. of ADT/COMPASS’95. Lecture notes in computer science, vol 1130. Springer, Berlin · Zbl 0962.68112
[36] Webber M (1996) Combining statecharts and Z for the design of safety-critical control systems. In: Proc. of FME’96. Lecture notes in computer science, vol 1051. Springer, Berlin
[37] Woodcock J (1990) Mathematics as a management tool: proof rules for promotion. In: Software engineering for large software systems. Springer, Netherlands · Zbl 1165.68048
[38] Woodcock J, Davies J (1996) Using Z: specification, refinement, and proof. Prentice Hall, Englewood Cliffs · Zbl 0855.68060
[39] Woodcock J, Cavancanti A (2001) Circus: a concurrent refinement language. Technical report, Oxford University Computing Laboratory, Oxford, UK
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.