(Heterogeneous) Structured specifications in logics without interpolation

"The world of software development has become intrinsically heterogeneous. Many formal languages have been made available to help analysts and designers model different aspects of software. Some examples in the logic realm are equational logic and classical rst-order logic, propositional tempo...

Descripción completa

Detalles Bibliográficos
Autores principales: López Pombo, Carlos G., Frías, Marcelo
Formato: Capítulos de libro acceptedVersion
Lenguaje:Inglés
Publicado: 2020
Materias:
INGENIERIA DE SOFTWARE
LENGUAJES DE ESPECIFICACION
LOGICA
ALGEBRA
Acceso en línea:http://ri.itba.edu.ar/handle/123456789/1926
Aporte de:
Repositorio Institucional Instituto Tecnológico de Buenos Aires (ITBA) de Instituto Tecnológico de Buenos Aires (ITBA)
id I32-R138-123456789-1926
record_format dspace
spelling I32-R138-123456789-19262022-12-07T13:14:59Z (Heterogeneous) Structured specifications in logics without interpolation López Pombo, Carlos G. Frías, Marcelo INGENIERIA DE SOFTWARE LENGUAJES DE ESPECIFICACION LOGICA ALGEBRA "The world of software development has become intrinsically heterogeneous. Many formal languages have been made available to help analysts and designers model different aspects of software. Some examples in the logic realm are equational logic and classical rst-order logic, propositional temporal logics such as LTL and CTL (and their rst-order versions), multimodal logics such as the dynamic logic PDL and its rst-order version, etc. One important feature of a specification language is the existence of structuring mechanisms enabling the modular construction of system descriptions. Structured specifications were introduced by Wirsing for rst-order logic, and later presented in the language-independent setting of institutions by Sannella and Tarlecki. Afterwards, Borzyszkowski presented suffcient conditions for a calculus for (homogeneous) structured speci cations to be complete. These conditions include some form of Craig's interpolation, which results in a scenario that excludes many formalisms employed in the description of software. The contributions of this article are then summarised as follows: a) We present a calculus for structured specifications whose completeness proof does not require any form of interpolation. b)We extend this calculus to a complete calculus for heterogeneous structured specifications." 2020-04-02T18:31:06Z 2020-04-02T18:31:06Z 2018 Capítulos de libro info:eu-repo/semantics/acceptedVersion 978-3319-97-878-9 http://ri.itba.edu.ar/handle/123456789/1926 en info:eu-repo/semantics/altIdentifier/doi/10.1007/978-3-319-97879-6_16 application/pdf
institution Instituto Tecnológico de Buenos Aires (ITBA)
institution_str I-32
repository_str R-138
collection Repositorio Institucional Instituto Tecnológico de Buenos Aires (ITBA)
language Inglés
topic INGENIERIA DE SOFTWARE
LENGUAJES DE ESPECIFICACION
LOGICA
ALGEBRA
spellingShingle INGENIERIA DE SOFTWARE
LENGUAJES DE ESPECIFICACION
LOGICA
ALGEBRA
López Pombo, Carlos G.
Frías, Marcelo
(Heterogeneous) Structured specifications in logics without interpolation
topic_facet INGENIERIA DE SOFTWARE
LENGUAJES DE ESPECIFICACION
LOGICA
ALGEBRA
description "The world of software development has become intrinsically heterogeneous. Many formal languages have been made available to help analysts and designers model different aspects of software. Some examples in the logic realm are equational logic and classical rst-order logic, propositional temporal logics such as LTL and CTL (and their rst-order versions), multimodal logics such as the dynamic logic PDL and its rst-order version, etc. One important feature of a specification language is the existence of structuring mechanisms enabling the modular construction of system descriptions. Structured specifications were introduced by Wirsing for rst-order logic, and later presented in the language-independent setting of institutions by Sannella and Tarlecki. Afterwards, Borzyszkowski presented suffcient conditions for a calculus for (homogeneous) structured speci cations to be complete. These conditions include some form of Craig's interpolation, which results in a scenario that excludes many formalisms employed in the description of software. The contributions of this article are then summarised as follows: a) We present a calculus for structured specifications whose completeness proof does not require any form of interpolation. b)We extend this calculus to a complete calculus for heterogeneous structured specifications."
format Capítulos de libro
acceptedVersion
author López Pombo, Carlos G.
Frías, Marcelo
author_facet López Pombo, Carlos G.
Frías, Marcelo
author_sort López Pombo, Carlos G.
title (Heterogeneous) Structured specifications in logics without interpolation
title_short (Heterogeneous) Structured specifications in logics without interpolation
title_full (Heterogeneous) Structured specifications in logics without interpolation
title_fullStr (Heterogeneous) Structured specifications in logics without interpolation
title_full_unstemmed (Heterogeneous) Structured specifications in logics without interpolation
title_sort (heterogeneous) structured specifications in logics without interpolation
publishDate 2020
url http://ri.itba.edu.ar/handle/123456789/1926
work_keys_str_mv AT lopezpombocarlosg heterogeneousstructuredspecificationsinlogicswithoutinterpolation
AT friasmarcelo heterogeneousstructuredspecificationsinlogicswithoutinterpolation
_version_ 1765661098893115392

Ejemplares similares