Tesis Doctorales UPM: Consulta online

Resumen: 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 especificación de una ecuación del futuro programa a derivar. El método deductivo desarrollado está basado en uno previo de Manna y 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 tipos y permite demostrar una especificación mediante varios cuadros. Cada cuadro demuestra una subespecificación y, por tanto, deriva una ecuación del programa. La tesis se completa con mecanismos para que los programas derivados puedan contener definiciones locales con patrones y variables sinónimas y anónimas, con varios ejemplos de aplicación y un análisis funcional de un entorno interactivo de derivación deductiva

Tesis: