Derivación deductiva de programas funcionales con patrones

Resumen

Una de las dificultades principales en el desarrollo de
software es la ausencia de un marco conceptual adecuado para
su estudio. Una propuesta la constituye el modelo transformativo,
que entiende el desarrollo de software como un proceso
iterativo de transformación de especificaciones: se parte de
una especificación inicial que va transformándose sucesivamente
hasta obtener una especificación final que se toma como
programa. Este modelo básico puede llevarse a la práctica de
varias maneras. En concreto, la aproximación deductiva toma
una sentencia lógica como especificación inicial y su proceso
transformador consiste en la demostración de la sentencia;
como producto secundario de la demostración se deriva un programa
que satisface la especificación inicial.
La tesis desarrolla un método deductivo para la derivación
de programas funcionales con patrones, escritos en un lenguaje
similar a Hope. El método utiliza una lógica multigénero, cuya
relación con el lenguaje de programación es estudiada. También
se identifican los esquemas de demostración necesarios para la
derivación de funciones con patrones, basados en la demostración
independiente de varias subsentencias. Cada subsentencia
proporciona una subespecificación de una ecuación del futuro
programa a derivar.
Nuestro método deductivo está inspirado en uno previo de
Zohar Manna y Richard Waldinger, conocido como el cuadro
deductivo, que deriva programas en un lenguaje similar a Lisp.
El nuevo método es una modificación del cuadro de estos autores,
que incorpora géneros y permite demostrar una especificación
mediante varios cuadros. Cada cuadro demuestra una subespecificación
y por tanto deriva una ecuación del programa. Se
prevén mecanismos para que los programas derivados puedan contener
definiciones locales con patrones y variables anónimas y
sinónimas y para que las funciones auxiliares derivadas no
usen variables de las funciones principales.
La tesis se completa con varios ejemplos de aplicación, un
mecanismo que independentiza el método del lenguaje de programación
y un prototipo de entorno interactivo de derivación
deductiva.
Categorías y descriptores de materia CR
D.l.l [Técnicas de programación]: Programación funcional;
D.2.10 [Ingeniería de software]: Diseño - métodos; F.3.1
[Lógica y significado de los programas]: Especificación, verificación
y razonamiento sobre programas - lógica de programas;
F.3.3 [Lógica y significado de los programas]: Estudios de
construcciones de programas - construcciones funcionales;
esquemas de programa y de recursion; 1.2.2 [Inteligencia artificial]:
Programación automática - síntesis de programas;
1.2.3 [Inteligencia artificial]: Deducción y demostración de
teoremas]: extracción de respuesta/razón; inducción matemática.
Términos generales
Programación funcional, síntesis de programas, demostración
de teoremas.
Otras palabras claves y expresiones
Funciones con patrones, cuadro deductivo, especificación
parcial, inducción estructural, teorema de descomposición.---ABSTRACT---One of the main difficulties in software development is
the lack of an adequate conceptual framework of study. The
transformational model is one such proposal that conceives
software development as an iterative process of specifications
transformation: an initial specification is developed and
successively transformed until a final specification is
obtained and taken as a program. This basic model can be
implemented in several ways. The deductive approach takes a
logical sentence as the initial specification and its proof
constitutes the transformational process; as a byproduct of
the proof, a program which satisfies the initial specification
is derived.
In the thesis, a deductive method for the derivation of
Hope-like functional programs with patterns is developed. The
method uses a many-sorted logic, whose relation to the
programming language is studied. Also the proof schemes necessary
for the derivation of functional programs with patterns,
based on the independent proof of several subsentences, are
identified. Each subsentence provides a subspecification of
one equation of the future program to be derived.
Our deductive method is inspired on a previous one by
Zohar Manna and Richard Waldinger, known as the deductive
tableau, which derives Lisp-like programs. The new method
incorporates sorts in the tableau and allows to prove a sentence
with several tableaux. Each tableau proves a subspecification
and therefore derives an equation of the program.
Mechanisms are included to allow the derived programs to contain
local definitions with patterns and anonymous and synonymous
variables; also, the derived auxiliary functions cannot
reference parameters of their main functions.
The thesis is completed with several application examples,
i mechanism to make the method independent from the
programming language and an interactive environment prototype
for deductive derivation.
CR categories and subject descriptors
D.l.l [Programming techniques]: Functional programming;
D.2.10 [Software engineering]: Design - methodologies; F.3.1
[Logics and meanings of programa]: Specifying and verifying
and reasoning about programs - logics of programs; F.3.3
[Logics and meanings of programs]: Studies of program constructs
- functional constructs; program and recursion schemes;
1.2.2 [Artificial intelligence]: Automatic programming - program
synthesis; 1.2.3 [Artificial intelligence]: Deduction and
theorem proving - answer/reason extraction; mathematical
induction.
General tenas
Functional programming, program synthesis, theorem proving.
Additional key words and phrases
Functions with patterns, deductive tableau, structural
induction, partial specification, descomposition theorem.