Navegar

Colección

Datos Estadísticas

Artículo

Castro, P.F.; Aguirre, N.; López Pombo, C.G.; Maibaum, T. "A categorical approach to structuring and promoting Z specifications" (2013) 9th International Symposium on Formal Aspects of Component Software, FACS 2012. 7684 LNCS:73-91
La versión final de este artículo es de uso interno. El editor solo permite incluir en el repositorio el artículo en su versión post-print. Por favor, si usted la posee enviela a
Consulte el artículo en la página del editor
Consulte la política de Acceso Abierto del editor

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