From Specifications to Programs: A Fork-Algebraic Approach to Bridge the Gap

The development of programs from first-order specifications has as its main difficulty that of dealing with universal quantifiers. This work is focused in that point, i.e., in the construction of programs whose specifications involve universal quantifiers. This task is performed within a relational...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autores principales: Baum, Gabriel Alfredo, Frias, Marcelo F., Haeberer, Armando Martin, Martínez López, Pablo E.
Formato: Objeto de conferencia
Lenguaje:Español
Publicado: 1996
Materias:
Informática
Acceso en línea:http://sedici.unlp.edu.ar/handle/10915/137421
Aporte de:
SEDICI (UNLP) de Universidad Nacional de La Plata
id I19-R120-10915-137421
record_format dspace
institution Universidad Nacional de La Plata
institution_str I-19
repository_str R-120
collection SEDICI (UNLP)
language Español
topic Informática
spellingShingle Informática
Baum, Gabriel Alfredo
Frias, Marcelo F.
Haeberer, Armando Martin
Martínez López, Pablo E.
From Specifications to Programs: A Fork-Algebraic Approach to Bridge the Gap
topic_facet Informática
description The development of programs from first-order specifications has as its main difficulty that of dealing with universal quantifiers. This work is focused in that point, i.e., in the construction of programs whose specifications involve universal quantifiers. This task is performed within a relational calculus based on fork algebras. The fact that first-order theories can be translated into equational theories in abstract fork algebras suggests that such work can be accomplished in a satisfactory way. Furthermore, the fact that these abstract algebras are representable guarantees that all properties valid in the standard models are captured by the axiomatization given for them, allowing the reasoning formalism to be shifted back and forth between any model and the abstract algebra. In order to cope with universal quantifiers, a new algebraic operation — relational implication — is introduced. This operation is shown to have deep significance in the relational statement of first-order expressions involving universal quantifiers. Several algebraic properties of the relational implication are stated showing its usefulness in program calculation. Finally, a non-trivial example of derivation is given to asses the merits of the relational implication as an specification tool, and also in calculation steps, where its algebraic properties are clearly appropriate as transformation rules.
format Objeto de conferencia
Objeto de conferencia
author Baum, Gabriel Alfredo
Frias, Marcelo F.
Haeberer, Armando Martin
Martínez López, Pablo E.
author_facet Baum, Gabriel Alfredo
Frias, Marcelo F.
Haeberer, Armando Martin
Martínez López, Pablo E.
author_sort Baum, Gabriel Alfredo
title From Specifications to Programs: A Fork-Algebraic Approach to Bridge the Gap
title_short From Specifications to Programs: A Fork-Algebraic Approach to Bridge the Gap
title_full From Specifications to Programs: A Fork-Algebraic Approach to Bridge the Gap
title_fullStr From Specifications to Programs: A Fork-Algebraic Approach to Bridge the Gap
title_full_unstemmed From Specifications to Programs: A Fork-Algebraic Approach to Bridge the Gap
title_sort from specifications to programs: a fork-algebraic approach to bridge the gap
publishDate 1996
url http://sedici.unlp.edu.ar/handle/10915/137421
work_keys_str_mv AT baumgabrielalfredo fromspecificationstoprogramsaforkalgebraicapproachtobridgethegap
AT friasmarcelof fromspecificationstoprogramsaforkalgebraicapproachtobridgethegap
AT haebererarmandomartin fromspecificationstoprogramsaforkalgebraicapproachtobridgethegap
AT martinezlopezpabloe fromspecificationstoprogramsaforkalgebraicapproachtobridgethegap
bdutipo_str Repositorios
_version_ 1764820456952561664

Ejemplares similares