Categorical foundations for structured specifications in $${\mathsf{Z}}$$ Z
| LEADER | caa a22 4500 | ||
|---|---|---|---|
| 001 | 605516227 | ||
| 003 | CHVBK | ||
| 005 | 20210128100713.0 | ||
| 007 | cr unu---uuuuu | ||
| 008 | 210128e20151101xx s 000 0 eng | ||
| 024 | 7 | 0 | |a 10.1007/s00165-015-0336-0 |2 doi |
| 035 | |a (NATIONALLICENCE)springer-10.1007/s00165-015-0336-0 | ||
| 245 | 0 | 0 | |a Categorical foundations for structured specifications in $${\mathsf{Z}}$$ Z |h [Elektronische Daten] |c [Pablo Castro, Nazareno Aguirre, Carlos Pombo, T. Maibaum] |
| 520 | 3 | |a 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 . | |
| 540 | |a British Computer Society, 2015 | ||
| 690 | 7 | |a Z Notation |2 nationallicence | |
| 690 | 7 | |a System specification |2 nationallicence | |
| 690 | 7 | |a System verification |2 nationallicence | |
| 690 | 7 | |a Category theory |2 nationallicence | |
| 690 | 7 | |a Heterogeneous specifications |2 nationallicence | |
| 700 | 1 | |a Castro |D Pablo |u Departamento de Computación, FCEFQyN, Universidad Nacional de Río Cuarto, Ruta Nac. No. 36 Km. 601, 5800, Río Cuarto, Córdoba, Argentina |4 aut | |
| 700 | 1 | |a Aguirre |D Nazareno |u Departamento de Computación, FCEFQyN, Universidad Nacional de Río Cuarto, Ruta Nac. No. 36 Km. 601, 5800, Río Cuarto, Córdoba, Argentina |4 aut | |
| 700 | 1 | |a Pombo |D Carlos |u Departamento de Computación, FCEyN, Universidad de Buenos Aires, Buenos Aires, Argentina |4 aut | |
| 700 | 1 | |a Maibaum |D T. |u Department of Computing and Software, McMaster University, Hamilton, ON, Canada |4 aut | |
| 773 | 0 | |t Formal Aspects of Computing |d Springer London |g 27/5-6(2015-11-01), 831-865 |x 0934-5043 |q 27:5-6<831 |1 2015 |2 27 |o 165 | |
| 856 | 4 | 0 | |u https://doi.org/10.1007/s00165-015-0336-0 |q text/html |z Onlinezugriff via DOI |
| 898 | |a BK010053 |b XK010053 |c XK010000 | ||
| 900 | 7 | |a Metadata rights reserved |b Springer special CC-BY-NC licence |2 nationallicence | |
| 908 | |D 1 |a research-article |2 jats | ||
| 949 | |B NATIONALLICENCE |F NATIONALLICENCE |b NL-springer | ||
| 950 | |B NATIONALLICENCE |P 856 |E 40 |u https://doi.org/10.1007/s00165-015-0336-0 |q text/html |z Onlinezugriff via DOI | ||
| 950 | |B NATIONALLICENCE |P 700 |E 1- |a Castro |D Pablo |u Departamento de Computación, FCEFQyN, Universidad Nacional de Río Cuarto, Ruta Nac. No. 36 Km. 601, 5800, Río Cuarto, Córdoba, Argentina |4 aut | ||
| 950 | |B NATIONALLICENCE |P 700 |E 1- |a Aguirre |D Nazareno |u Departamento de Computación, FCEFQyN, Universidad Nacional de Río Cuarto, Ruta Nac. No. 36 Km. 601, 5800, Río Cuarto, Córdoba, Argentina |4 aut | ||
| 950 | |B NATIONALLICENCE |P 700 |E 1- |a Pombo |D Carlos |u Departamento de Computación, FCEyN, Universidad de Buenos Aires, Buenos Aires, Argentina |4 aut | ||
| 950 | |B NATIONALLICENCE |P 700 |E 1- |a Maibaum |D T. |u Department of Computing and Software, McMaster University, Hamilton, ON, Canada |4 aut | ||
| 950 | |B NATIONALLICENCE |P 773 |E 0- |t Formal Aspects of Computing |d Springer London |g 27/5-6(2015-11-01), 831-865 |x 0934-5043 |q 27:5-6<831 |1 2015 |2 27 |o 165 | ||