INVESTIGADORES
FRIAS Marcelo Fabian
artículos
Título:
From Specifications to Programs: A Fork Algebraic Approach to Bridge the Gap
Autor/es:
BAUM, GABRIEL; FRIAS, MARCELO FABIAN; HAEBERER, ARMANDO MARTIN; MARTINEZ LOPEZ, PABLO
Revista:
LECTURE NOTES IN COMPUTER SCIENCE
Editorial:
Springer
Referencias:
Año: 1996 vol. 1113 p. 180 - 191
ISSN:
0302-9743
Resumen:
The development of programs from firstorder 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 firstorder 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 firstorder expressions involving universal quantifiers. Several algebraic properties of the relational implication are stated showing its usefulness in program calculation. Finally, a nontrivial 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.