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.
Reviewer: Răzvan Diaconescu (Ploiesti)
MSC:
| 68Q65 | Abstract data types; algebraic specification |
Keywords:
\(\mathsf{Z}\) notation; system specification; system verification; category theory; heterogeneous specifications; institutionReferences:
| [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 · Zbl 1375.18001 |
| [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 (2000) A calculus for schemas in Z. J Symb Comput 30(1): 63-91 · Zbl 0962.68112 · doi:10.1006/jsco.1999.0347 |
| [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 · Zbl 0697.03022 |
| [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 (1992) Temporal theories as modularisation units for concurrent system specification. Form Asp Comput 4(3): 239-272 · Zbl 0746.68031 · doi:10.1007/BF01212304 |
| [14] | Finkelstein A, Kramer J, Nuseibeh B, Finkelstein L, Goedicke M (1992) Viewpoints: a framework for integrating multiple perspectives in system development. Int J Softw Eng Knowl Eng 2(1): 31-57 · doi:10.1142/S0218194092000038 |
| [15] | Fischer C (1997) Combining CSP and Z. Technical Report, University of Oldenburg |
| [16] | Goguen J, Burstall R (1992) Institutions: abstract model theory for specification and programming. J ACM 39(1): 95-146 · Zbl 0799.68134 · doi:10.1145/147508.147524 |
| [17] | Henson M, Reeves S (1999) Revising Z: part I—logic and semantics. Form Asp Comput 11(4): 359-380 · Zbl 0955.68077 · doi:10.1007/s001650050038 |
| [18] | Henson M, Reeves S (1999) Revising Z: part II—logical development. Form Asp Comput 11(4): 381-401 · Zbl 0955.68078 · doi:10.1007/s001650050039 |
| [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 (2009) A UTP semantics for circus. Form Asp Comput 21(2): 3-32 · Zbl 1165.68048 · doi:10.1007/s00165-007-0052-5 |
| [29] | Parnas D (1972) On the criteria to be used in decomposing systems into modules. Commun. ACM 15(12): 1053-1058 · doi:10.1145/361598.361623 |
| [30] | Parnas D (1985) The modular structure of complex system. IEEE Trans Softw Eng 11(3): 259-266 · doi:10.1109/TSE.1985.232209 |
| [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 · Zbl 0777.68003 |
| [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. 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.
