A categorical approach to structuring and promoting Z specifications

Mostrar otras versiones (1)

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 typ...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autor principal: Castro, P.F
Otros Autores: Aguirre, N., López Pombo, C.G, Maibaum, T.
Formato: Acta de conferencia Capítulo de libro
Lenguaje:Inglés
Publicado: 2013
Acceso en línea:Registro en Scopus
DOI
Handle
Registro en la Biblioteca Digital
Aporte de:Registro referencial: Solicitar el recurso aquí
Biblioteca Central Dr. Luis F. Leloir (FCEN) de Universidad de Buenos Aires
LEADER 07495caa a22008417a 4500
001 PAPER-11798
003 AR-BaUEN
005 20230518204159.0
008 190411s2013 xx ||||fo|||| 00| 0 eng|d
024 7 |2 scopus  |a 2-s2.0-84872735522 
040 |a Scopus  |b spa  |c AR-BaUEN  |d AR-BaUEN 
100 1 |a Castro, P.F. 
245 1 2 |a A categorical approach to structuring and promoting Z specifications 
260 |c 2013 
270 1 0 |m Castro, P.F.; Departamento de Computación, FCEFQyN, Universidad Nacional de Río Cuarto, Río Cuarto, Córdoba, Argentina; email: pcastro@dc.exa.unrc.edu.ar 
506 |2 openaire  |e Política editorial 
504 |a Abrial, J.-R., (1996) The B-Book, Assigning Programs to Meanings, , Cambridge University Press 
504 |a Barr, M., Wells, C., (1999) Category Theory for Computer Science, , Centre de Recherches Mathématiques, Université de Montréal 
504 |a 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 
504 |a Bérnabou, J., Introduction to bicategories (1967) LNM, 42. , Complementary Definitions of Programming Language Semantics. Springer 
504 |a Borceux, F., Handbook of Categorical Algebra: Volume 1: Basic Category Theory (1994) Enc. of Mathematics and Its Applications, , Cambridge University Press 
504 |a Brien, S.M., Martin, A.P., A Calculus for Schemas in Z (2000) Journal of Symbolic Computation, 30 (1) 
504 |a 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 
504 |a Burstall, R., Goguen, J., Putting Theories together to make Specifications Proc. of Intl. Joint Conference on Artificial Intelligence (1977) 
504 |a 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 
504 |a Chang, C.C., Keisler, H.J., (1990) Model Theory, , 3rd edn. North-Holland 
504 |a Enderton, H., (2001) A Mathematical Introduction to Logic, , 2nd edn. Academic Press 
504 |a Fiadeiro, J., (2004) Categories for Software Engineering, , Springer 
504 |a Fiadeiro, J., Maibaum, T., Temporal Theories as Modularisation Units for Concurrent System Specification (1992) Formal Aspects of Computing, 4 (3) 
504 |a Fischer, C., (1997) Combining CSP and Z, , Technical Report, University of Oldenburg 
504 |a Goguen, J., Burstall, R., Institutions: Abstract Model Theory for Specification and Programming (1992) Journal of the ACM, 39 (1) 
504 |a Henson, M., Reeves, S., Revising Z: Part I - Logic and Semantics (1999) Formal Aspects of Computing, 11 (4) 
504 |a Nicholls, J., (1995) Z Notation: Version 1.2, , Z Standards Panel 
504 |a 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 
504 |a 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 
504 |a Smith, G., The Object Z Specification Language (2000) Advances in Formal Methods Series, , Kluwer Academic Publishers 
504 |a Spivey, J.M., Understanding Z: A Specification Language and its Formal Semantics (1988) Cambridge Tracts in Theoretical Computer Science 
504 |a Spivey, J.M., (1992) The Z Notation: A Reference Manual, , Prentice Hall 
504 |a 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 
504 |a 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 
504 |a Woodcock, J., Davies, J., (1996) Using Z: Specification, Refinement, and Proof, , Prentice Hall 
520 3 |a 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.  |l eng 
593 |a Departamento de Computación, FCEFQyN, Universidad Nacional de Río Cuarto, Río Cuarto, Córdoba, Argentina 
593 |a Departamento de Computación, FCEyN, Universidad de Buenos Aires, Buenos Aires, Argentina 
593 |a Consejo Nacional de Investigaciones Científicas Y Técnicas (CONICET), Argentina 
593 |a Department of Computing and Software, McMaster University, Hamilton, ON, Canada 
690 1 0 |a ABSTRACT NOTIONS 
690 1 0 |a CATEGORY THEORY 
690 1 0 |a FORMAL FOUNDATION 
690 1 0 |a FORMALISATION 
690 1 0 |a LOGICAL SYSTEM 
690 1 0 |a PROPERTY PRESERVATION 
690 1 0 |a SCHEMA OPERATORS 
690 1 0 |a SEMANTIC RELATIONSHIPS 
690 1 0 |a STRUCTURING MECHANISMS 
690 1 0 |a SYNTACTIC TRANSFORMATIONS 
690 1 0 |a Z SPECIFICATIONS 
690 1 0 |a SEMANTICS 
690 1 0 |a SYNTACTICS 
690 1 0 |a COMPUTER SOFTWARE 
700 1 |a Aguirre, N. 
700 1 |a López Pombo, C.G. 
700 1 |a Maibaum, T. 
711 2 |c Mountain View, CA  |d 12 September 2012 through 14 September 2012  |g Código de la conferencia: 95095 
773 0 |d 2013  |g v. 7684 LNCS  |h pp. 73-91  |p Lect. Notes Comput. Sci.  |n Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)  |x 03029743  |w (AR-BaUEN)CENRE-983  |z 9783642358609  |t 9th International Symposium on Formal Aspects of Component Software, FACS 2012 
856 4 1 |u https://www.scopus.com/inward/record.uri?eid=2-s2.0-84872735522&doi=10.1007%2f978-3-642-35861-6_5&partnerID=40&md5=493f4902140a0fae6944add6ce9e245b  |y Registro en Scopus 
856 4 0 |u https://doi.org/10.1007/978-3-642-35861-6_5  |y DOI 
856 4 0 |u https://hdl.handle.net/20.500.12110/paper_03029743_v7684LNCS_n_p73_Castro  |y Handle 
856 4 0 |u https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v7684LNCS_n_p73_Castro  |y Registro en la Biblioteca Digital 
961 |a paper_03029743_v7684LNCS_n_p73_Castro  |b paper  |c PE 
962 |a info:eu-repo/semantics/article  |a info:ar-repo/semantics/artículo  |b info:eu-repo/semantics/publishedVersion 
963 |a VARI 
999 |c 72751 

Ejemplares similares