A categorical approach to structuring and promoting Z specifications

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:	López Pombo, Carlos Gustavo
Publicado:	2013
Materias:	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
Acceso en línea:	https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v7684LNCS_n_p73_Castro http://hdl.handle.net/20.500.12110/paper_03029743_v7684LNCS_n_p73_Castro
Aporte de:	Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires

id	paper:paper_03029743_v7684LNCS_n_p73_Castro
record_format	dspace
spelling	paper:paper_03029743_v7684LNCS_n_p73_Castro2023-06-08T15:28:49Z A categorical approach to structuring and promoting Z specifications López Pombo, Carlos Gustavo 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 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. Fil:López Pombo, C.G. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. 2013 https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v7684LNCS_n_p73_Castro http://hdl.handle.net/20.500.12110/paper_03029743_v7684LNCS_n_p73_Castro
institution	Universidad de Buenos Aires
institution_str	I-28
repository_str	R-134
collection	Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA)
topic	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
spellingShingle	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 López Pombo, Carlos Gustavo A categorical approach to structuring and promoting Z specifications
topic_facet	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
description	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.
author	López Pombo, Carlos Gustavo
author_facet	López Pombo, Carlos Gustavo
author_sort	López Pombo, Carlos Gustavo
title	A categorical approach to structuring and promoting Z specifications
title_short	A categorical approach to structuring and promoting Z specifications
title_full	A categorical approach to structuring and promoting Z specifications
title_fullStr	A categorical approach to structuring and promoting Z specifications
title_full_unstemmed	A categorical approach to structuring and promoting Z specifications
title_sort	categorical approach to structuring and promoting z specifications
publishDate	2013
url	https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v7684LNCS_n_p73_Castro http://hdl.handle.net/20.500.12110/paper_03029743_v7684LNCS_n_p73_Castro
work_keys_str_mv	AT lopezpombocarlosgustavo acategoricalapproachtostructuringandpromotingzspecifications AT lopezpombocarlosgustavo categoricalapproachtostructuringandpromotingzspecifications
_version_	1768545555215024128

A categorical approach to structuring and promoting Z specifications

Ejemplares similares