Abstract
In this paper, we study a formalisation of specification structuring mechanisms used in Z. These mechanisms are traditionally understood as syntactic transformations. In contrast, we present a characterisation of Z structuring mechanisms which takes into account the semantic counterpart of their typical syntactic descriptions, based on category theory. Our formal foundation for Z employs well established abstract notions of logical systems. This setting has a degree of abstraction that enables us to understand what is the precise semantic relationship between schemas obtained from a schema operator and the schemas it is applied to, in particular with respect to property preservation.
Our formalisation is a powerful setting for capturing structuring mechanisms, even enabling us to formalise promotion. Also, its abstract nature provides the rigour and flexibility needed to characterise extensions of Z and related languages, in particular the heterogeneous ones.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abrial, J.-R.: The B-Book, Assigning Programs to Meanings. Cambridge University Press (1996)
Barr, M., Wells, C.: Category Theory for Computer Science, Centre de Recherches Mathématiques, Université de Montréal (1999)
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)
Bérnabou, J.: Introduction to bicategories. In: Complementary Definitions of Programming Language Semantics. LNM, vol. 42. Springer (1967)
Borceux, F.: Handbook of Categorical Algebra: Volume 1: Basic Category Theory. Enc. of Mathematics and its Applications. Cambridge University Press (1994)
Brien, S.M., Martin, A.P.: A Calculus for Schemas in Z. Journal of Symbolic Computation 30(1) (2000)
Bujorianu, M.C.: Integration of Specification Languages Using Viewpoints. In: Boiten, E.A., Derrick, J., Smith, G.P. (eds.) IFM 2004. LNCS, vol. 2999, pp. 421–440. Springer, Heidelberg (2004)
Burstall, R., Goguen, J.: Putting Theories together to make Specifications. In: Proc. of Intl. Joint Conference on Artificial Intelligence (1977)
Castro, P.F., Aguirre, N.M., López Pombo, C.G., Maibaum, T.S.E.: Towards Managing Dynamic Reconfiguration of Software Systems in a Categorical Setting. In: Cavalcanti, A., Deharbe, D., Gaudel, M.-C., Woodcock, J. (eds.) ICTAC 2010. LNCS, vol. 6255, pp. 306–321. Springer, Heidelberg (2010)
Chang, C.C., Keisler, H.J.: Model Theory, 3rd edn. North-Holland (1990)
Enderton, H.: A Mathematical Introduction to Logic, 2nd edn. Academic Press (2001)
Fiadeiro, J.: Categories for Software Engineering. Springer (2004)
Fiadeiro, J., Maibaum, T.: Temporal Theories as Modularisation Units for Concurrent System Specification. Formal Aspects of Computing 4(3) (1992)
Fischer, C.: Combining CSP and Z, Technical Report, University of Oldenburg (1997)
Goguen, J., Burstall, R.: Institutions: Abstract Model Theory for Specification and Programming. Journal of the ACM, 39(1) (1992)
Henson, M., Reeves, S.: Revising Z: Part I - Logic and Semantics. Formal Aspects of Computing 11(4) (1999)
Nicholls, J.: Z Notation: Version 1.2, Z Standards Panel (1995)
Mossakowski, T., Tarlecki, A., Pawlowski, W.: Combining and Representing Logical Systems. In: Moggi, E., Rosolini, G. (eds.) CTCS 1997. LNCS, vol. 1290, pp. 177–196. Springer, Heidelberg (1997)
Mossakowski, T., Roggenbach, M.: Structured CSP – A Process Algebra as an Institution. In: Fiadeiro, J.L., Schobbens, P.-Y. (eds.) WADT 2006. LNCS, vol. 4409, pp. 92–110. Springer, Heidelberg (2007)
Smith, G.: The Object Z Specification Language. Advances in Formal Methods Series. Kluwer Academic Publishers (2000)
Spivey, J.M.: Understanding Z: A Specification Language and its Formal Semantics. Cambridge Tracts in Theoretical Computer Science (1988)
Spivey, J.M.: The Z Notation: A Reference Manual. Prentice Hall (1992)
Tarlecki, A.: Moving Between Logical Systems. In: Haveraaen, M., Dahl, O.-J., Owe, O. (eds.) ADT 1995 & COMPASS 1995. LNCS, vol. 1130, pp. 478–502. Springer, Heidelberg (1996)
Webber, M.: Combining Statecharts and Z for the Design of Safety-Critical Control Systems. In: Gaudel, M.-C., Wing, J.M. (eds.) FME 1996. LNCS, vol. 1051, pp. 307–326. Springer, Heidelberg (1996)
Woodcock, J., Davies, J.: Using Z: Specification, Refinement, and Proof. Prentice Hall (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Castro, P.F., Aguirre, N., López Pombo, C.G., Maibaum, T. (2013). A Categorical Approach to Structuring and Promoting Z Specifications. In: Păsăreanu, C.S., Salaün, G. (eds) Formal Aspects of Component Software. FACS 2012. Lecture Notes in Computer Science, vol 7684. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-35861-6_5
Download citation
DOI: https://doi.org/10.1007/978-3-642-35861-6_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-35860-9
Online ISBN: 978-3-642-35861-6
eBook Packages: Computer ScienceComputer Science (R0)