Estudio de la verificación de propiedades de programas funcionales de las pruebas manuales al uso de asistentes de pruebas

Resumo

El principal objetivo de esta tesis es la investigación de una metodología para producir software certificado, desde pruebas manuales hasta el uso de asistentes que supervisan y colaboran en el proceso de prueba, Estudiaremos el desarrollo de algoritmos probados formalmente para la computación, explicando cómo demostrar que una implementación de un algoritmo cumple las propiedades esperadas, realizando este examen en base al estudio de distintos ejemplos en orden creciente de complejidad, teniendo en cuenta no sólo la certificación de los programas sino tambien de su eficiencia. Para cada uno de estos programas, presentamos en primer lugar, todas las definiciones y demostraciones de propiedades con pruebas hechas a mano en un estilo riguroso, donde cada paso está justificado por razonamiento matemático, y a continuación presentamos una transformación de la formalización de estas definiciones y pruebas a otras equivalentes en el sistema de pruebas Coq. Como otros probadores de teoremas, este sistema proporciona control y asistencia durante los procesos de especificación y prueba; por tanto evita errores que podrían introducirse en una prueba a mano. El asistente de pruebas Coq es una implementación del cálculo de construcciones inductivas que es una teoría de tipos resultante de la combinación de la teoría intuicionista de tipos de Martin Lof y el cálculo polimórfico de Girard, Fw. La teoría constructiva de tipos guarda similitudes con los lenguajes de programación. La prueba de un teorema es una función que a partir de las pruebas de las hipótesis del teorema, calcula la prueba del enunciado. Así, las formalizaciones de los algoritmos en Coq son compilables eficientemente usándose para la computación. Las técnicas propuestas quedarán ejemplificadas sobre programas no triviales, donde se describen formalmente los principios básico que hacen a estos algoritmos funcionar, quedando manifiesta la posibilidad de