caa a22 4500 605516227 CHVBK 20210128100713.0 cr unu---uuuuu 210128e20151101xx s 000 0 eng 10.1007/s00165-015-0336-0 doi (NATIONALLICENCE)springer-10.1007/s00165-015-0336-0 Categorical foundations for structured specifications in $${\mathsf{Z}}$$ Z [Elektronische Daten] [Pablo Castro, Nazareno Aguirre, Carlos Pombo, T. Maibaum] In this paper we present a formalization of the $${\mathsf{Z}}$$ 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 $${\mathsf{Z}}$$ Z and its related concepts. We show that the main structuring mechanisms of $${\mathsf{Z}}$$ 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 $${\mathsf{Z}}$$ 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 $${\mathsf{Z}}$$ 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 $${\mathsf{Z}}$$ Z with $${\mathsf{CSP}}$$ CSP . British Computer Society, 2015 Z Notation nationallicence System specification nationallicence System verification nationallicence Category theory nationallicence Heterogeneous specifications nationallicence Castro Pablo Departamento de Computación, FCEFQyN, Universidad Nacional de Río Cuarto, Ruta Nac. No. 36 Km. 601, 5800, Río Cuarto, Córdoba, Argentina aut Aguirre Nazareno Departamento de Computación, FCEFQyN, Universidad Nacional de Río Cuarto, Ruta Nac. No. 36 Km. 601, 5800, Río Cuarto, Córdoba, Argentina aut Pombo Carlos Departamento de Computación, FCEyN, Universidad de Buenos Aires, Buenos Aires, Argentina aut Maibaum T. Department of Computing and Software, McMaster University, Hamilton, ON, Canada aut Formal Aspects of Computing Springer London 27/5-6(2015-11-01), 831-865 0934-5043 27:5-6<831 2015 27 165 https://doi.org/10.1007/s00165-015-0336-0 text/html Onlinezugriff via DOI BK010053 XK010053 XK010000 Metadata rights reserved Springer special CC-BY-NC licence nationallicence 1 research-article jats NATIONALLICENCE NATIONALLICENCE NL-springer NATIONALLICENCE 856 40 https://doi.org/10.1007/s00165-015-0336-0 text/html Onlinezugriff via DOI NATIONALLICENCE 700 1- Castro Pablo Departamento de Computación, FCEFQyN, Universidad Nacional de Río Cuarto, Ruta Nac. No. 36 Km. 601, 5800, Río Cuarto, Córdoba, Argentina aut NATIONALLICENCE 700 1- Aguirre Nazareno Departamento de Computación, FCEFQyN, Universidad Nacional de Río Cuarto, Ruta Nac. No. 36 Km. 601, 5800, Río Cuarto, Córdoba, Argentina aut NATIONALLICENCE 700 1- Pombo Carlos Departamento de Computación, FCEyN, Universidad de Buenos Aires, Buenos Aires, Argentina aut NATIONALLICENCE 700 1- Maibaum T. Department of Computing and Software, McMaster University, Hamilton, ON, Canada aut NATIONALLICENCE 773 0- Formal Aspects of Computing Springer London 27/5-6(2015-11-01), 831-865 0934-5043 27:5-6<831 2015 27 165