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. © 2013 Springer-Verlag.
Registro:
Documento: |
Artículo
|
Título: | A categorical approach to structuring and promoting Z specifications |
Autor: | Castro, P.F.; Aguirre, N.; López Pombo, C.G.; Maibaum, T. |
Ciudad: | Mountain View, CA |
Filiación: | Departamento de Computación, FCEFQyN, Universidad Nacional de Río Cuarto, Río Cuarto, Córdoba, Argentina Departamento de Computación, FCEyN, Universidad de Buenos Aires, Buenos Aires, Argentina Consejo Nacional de Investigaciones Científicas Y Técnicas (CONICET), Argentina Department of Computing and Software, McMaster University, Hamilton, ON, Canada
|
Palabras clave: | Abstract notions; Category theory; Formal foundation; Formalisation; Logical system; Property preservation; Schema operators; Semantic relationships; Structuring mechanisms; Syntactic transformations; Z specifications; Semantics; Syntactics; Computer software |
Año: | 2013
|
Volumen: | 7684 LNCS
|
Página de inicio: | 73
|
Página de fin: | 91
|
DOI: |
http://dx.doi.org/10.1007/978-3-642-35861-6_5 |
Título revista: | 9th International Symposium on Formal Aspects of Component Software, FACS 2012
|
Título revista abreviado: | Lect. Notes Comput. Sci.
|
ISSN: | 03029743
|
Registro: | https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v7684LNCS_n_p73_Castro |
Referencias:
- Abrial, J.-R., (1996) The B-Book, Assigning Programs to Meanings, , Cambridge University Press
- Barr, M., Wells, C., (1999) Category Theory for Computer Science, , Centre de Recherches Mathématiques, Université de Montréal
- Baumeister, H., Relating Abstract Datatypes and Z-Schemata (2000) LNCS, 1827, pp. 366-382. , Bert, D., Choppy, C., Mosses, P.D. (eds.) WADT 1999. Springer, Heidelberg
- Bérnabou, J., Introduction to bicategories (1967) LNM, 42. , Complementary Definitions of Programming Language Semantics. Springer
- Borceux, F., Handbook of Categorical Algebra: Volume 1: Basic Category Theory (1994) Enc. of Mathematics and Its Applications, , Cambridge University Press
- Brien, S.M., Martin, A.P., A Calculus for Schemas in Z (2000) Journal of Symbolic Computation, 30 (1)
- Bujorianu, M.C., Integration of Specification Languages Using Viewpoints (2004) LNCS, 2999, pp. 421-440. , Boiten, E.A., Derrick, J., Smith, G.P. (eds.) IFM 2004. Springer, Heidelberg
- Burstall, R., Goguen, J., Putting Theories together to make Specifications 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 (2010) LNCS, 6255, pp. 306-321. , Cavalcanti, A., Deharbe, D., Gaudel, M.-C., Woodcock, J. (eds.) ICTAC 2010. Springer, Heidelberg
- Chang, C.C., Keisler, H.J., (1990) Model Theory, , 3rd edn. North-Holland
- Enderton, H., (2001) A Mathematical Introduction to Logic, , 2nd edn. Academic Press
- Fiadeiro, J., (2004) Categories for Software Engineering, , Springer
- Fiadeiro, J., Maibaum, T., Temporal Theories as Modularisation Units for Concurrent System Specification (1992) Formal Aspects of Computing, 4 (3)
- Fischer, C., (1997) Combining CSP and Z, , Technical Report, University of Oldenburg
- Goguen, J., Burstall, R., Institutions: Abstract Model Theory for Specification and Programming (1992) Journal of the ACM, 39 (1)
- Henson, M., Reeves, S., Revising Z: Part I - Logic and Semantics (1999) Formal Aspects of Computing, 11 (4)
- Nicholls, J., (1995) Z Notation: Version 1.2, , Z Standards Panel
- Mossakowski, T., Tarlecki, A., Pawlowski, W., Combining and Representing Logical Systems (1997) LNCS, 1290, pp. 177-196. , Moggi, E., Rosolini, G. (eds.) CTCS 1997. Springer, Heidelberg
- Mossakowski, T., Roggenbach, M., Structured CSP - A Process Algebra as an Institution (2007) LNCS, 4409, pp. 92-110. , Fiadeiro, J.L., Schobbens, P.-Y. (eds.) WADT 2006. Springer, Heidelberg
- Smith, G., The Object Z Specification Language (2000) Advances in Formal Methods Series, , Kluwer Academic Publishers
- Spivey, J.M., Understanding Z: A Specification Language and its Formal Semantics (1988) Cambridge Tracts in Theoretical Computer Science
- Spivey, J.M., (1992) The Z Notation: A Reference Manual, , Prentice Hall
- Tarlecki, A., Moving between Logical Systems (1996) LNCS, 1130, pp. 478-502. , Haveraaen, M., Dahl, O.-J., Owe, O. (eds.) ADT 1995 & COMPASS 1995. Springer, Heidelberg
- Webber, M., Combining Statecharts and Z for the Design of Safety-Critical Control Systems (1996) LNCS, 1051, pp. 307-326. , Gaudel, M.-C., Wing, J.M. (eds.) FME 1996. Springer, Heidelberg
- Woodcock, J., Davies, J., (1996) Using Z: Specification, Refinement, and Proof, , Prentice Hall
Citas:
---------- APA ----------
Castro, P.F., Aguirre, N., López Pombo, C.G. & Maibaum, T.
(2013)
. A categorical approach to structuring and promoting Z specifications. 9th International Symposium on Formal Aspects of Component Software, FACS 2012, 7684 LNCS, 73-91.
http://dx.doi.org/10.1007/978-3-642-35861-6_5---------- CHICAGO ----------
Castro, P.F., Aguirre, N., López Pombo, C.G., Maibaum, T.
"A categorical approach to structuring and promoting Z specifications"
. 9th International Symposium on Formal Aspects of Component Software, FACS 2012 7684 LNCS
(2013) : 73-91.
http://dx.doi.org/10.1007/978-3-642-35861-6_5---------- MLA ----------
Castro, P.F., Aguirre, N., López Pombo, C.G., Maibaum, T.
"A categorical approach to structuring and promoting Z specifications"
. 9th International Symposium on Formal Aspects of Component Software, FACS 2012, vol. 7684 LNCS, 2013, pp. 73-91.
http://dx.doi.org/10.1007/978-3-642-35861-6_5---------- VANCOUVER ----------
Castro, P.F., Aguirre, N., López Pombo, C.G., Maibaum, T. A categorical approach to structuring and promoting Z specifications. Lect. Notes Comput. Sci. 2013;7684 LNCS:73-91.
http://dx.doi.org/10.1007/978-3-642-35861-6_5