Categorical foundations for structured specifications in Z

In this paper we present a formalization of the Z notation and its structuring mechanisms. One of the main features of our formal framework, based on category theory and the theory of institutions, is that it enables us to provide an abstract view of Z and its related concepts. We show that the main...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autores principales: Castro, P.F., Aguirre, N., Pombo, C.L., Maibaum, T.S.E.
Formato: JOUR
Materias:
Category theory
Heterogeneous specifications
System specification
System verification
Z Notation
Calculations
Computational linguistics
Computer hardware description languages
Formal languages
Formal methods
Formal specification
Semantics
Formal framework
Mathematical formalism
Structured specification
Structuring mechanisms
System verifications
Z notation
Specifications
Acceso en línea:http://hdl.handle.net/20.500.12110/paper_09345043_v27_n5-6_p831_Castro
Aporte de:
Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires
id todo:paper_09345043_v27_n5-6_p831_Castro
record_format dspace
spelling todo:paper_09345043_v27_n5-6_p831_Castro2023-10-03T15:48:34Z Categorical foundations for structured specifications in Z Castro, P.F. Aguirre, N. Pombo, C.L. Maibaum, T.S.E. Category theory Heterogeneous specifications System specification System verification Z Notation Calculations Computational linguistics Computer hardware description languages Formal languages Formal methods Formal specification Semantics Category theory Formal framework Mathematical formalism Structured specification Structuring mechanisms System specification System verifications Z notation Specifications In this paper we present a formalization of the Z notation and its structuring mechanisms. One of the main features of our formal framework, based on category theory and the theory of institutions, is that it enables us to provide an abstract view of Z and its related concepts. We show that the main structuring mechanisms of Z are captured smoothly by categorical constructions. In particular, we provide a straightforward and clear semantics for promotion, a powerful structuring technique that is often not presented as part of the schema calculus. Here we show that promotion is already an operation over schemas (and more generally over specifications), that allows one to promote schemas that operate on a local notion of state to operate on a subsuming global state, and in particular can be used to conveniently define large specifications from collections of simpler ones. Moreover, our proposed formalization facilitates the combination of Z with other notations in order to produce heterogeneous specifications, i.e., specifications that are obtained by using various different mathematical formalisms. Thus, our abstract and precise formulation of Z is useful for relating this notation with other formal languages used by the formal methods community. We illustrate this by means of a known combination of formal languages, namely the combination of Z with CSP. © 2015, British Computer Society. JOUR info:eu-repo/semantics/openAccess http://creativecommons.org/licenses/by/2.5/ar http://hdl.handle.net/20.500.12110/paper_09345043_v27_n5-6_p831_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 Category theory
Heterogeneous specifications
System specification
System verification
Z Notation
Calculations
Computational linguistics
Computer hardware description languages
Formal languages
Formal methods
Formal specification
Semantics
Category theory
Formal framework
Mathematical formalism
Structured specification
Structuring mechanisms
System specification
System verifications
Z notation
Specifications
spellingShingle Category theory
Heterogeneous specifications
System specification
System verification
Z Notation
Calculations
Computational linguistics
Computer hardware description languages
Formal languages
Formal methods
Formal specification
Semantics
Category theory
Formal framework
Mathematical formalism
Structured specification
Structuring mechanisms
System specification
System verifications
Z notation
Specifications
Castro, P.F.
Aguirre, N.
Pombo, C.L.
Maibaum, T.S.E.
Categorical foundations for structured specifications in Z
topic_facet Category theory
Heterogeneous specifications
System specification
System verification
Z Notation
Calculations
Computational linguistics
Computer hardware description languages
Formal languages
Formal methods
Formal specification
Semantics
Category theory
Formal framework
Mathematical formalism
Structured specification
Structuring mechanisms
System specification
System verifications
Z notation
Specifications
description In this paper we present a formalization of the Z notation and its structuring mechanisms. One of the main features of our formal framework, based on category theory and the theory of institutions, is that it enables us to provide an abstract view of Z and its related concepts. We show that the main structuring mechanisms of Z are captured smoothly by categorical constructions. In particular, we provide a straightforward and clear semantics for promotion, a powerful structuring technique that is often not presented as part of the schema calculus. Here we show that promotion is already an operation over schemas (and more generally over specifications), that allows one to promote schemas that operate on a local notion of state to operate on a subsuming global state, and in particular can be used to conveniently define large specifications from collections of simpler ones. Moreover, our proposed formalization facilitates the combination of Z with other notations in order to produce heterogeneous specifications, i.e., specifications that are obtained by using various different mathematical formalisms. Thus, our abstract and precise formulation of Z is useful for relating this notation with other formal languages used by the formal methods community. We illustrate this by means of a known combination of formal languages, namely the combination of Z with CSP. © 2015, British Computer Society.
format JOUR
author Castro, P.F.
Aguirre, N.
Pombo, C.L.
Maibaum, T.S.E.
author_facet Castro, P.F.
Aguirre, N.
Pombo, C.L.
Maibaum, T.S.E.
author_sort Castro, P.F.
title Categorical foundations for structured specifications in Z
title_short Categorical foundations for structured specifications in Z
title_full Categorical foundations for structured specifications in Z
title_fullStr Categorical foundations for structured specifications in Z
title_full_unstemmed Categorical foundations for structured specifications in Z
title_sort categorical foundations for structured specifications in z
url http://hdl.handle.net/20.500.12110/paper_09345043_v27_n5-6_p831_Castro
work_keys_str_mv AT castropf categoricalfoundationsforstructuredspecificationsinz
AT aguirren categoricalfoundationsforstructuredspecificationsinz
AT pombocl categoricalfoundationsforstructuredspecificationsinz
AT maibaumtse categoricalfoundationsforstructuredspecificationsinz
_version_ 1807314903699030016

Ejemplares similares