Síntesis de programa
En ciencias de la computación , la síntesis de programas es la tarea de construir un programa que satisfaga de manera comprobable una especificación formal dada de alto nivel . A diferencia de la verificación del programa , el programa debe construirse más que darse; sin embargo, ambos campos hacen uso de técnicas de prueba formal y ambos comprenden enfoques de diferentes grados de automatización. A diferencia de las técnicas de programación automática , las especificaciones en la síntesis de programas suelen ser declaraciones no algorítmicas en un cálculo lógico apropiado . [1]
Durante el Instituto de Verano de Lógica Simbólica de la Universidad de Cornell en 1957, Alonzo Church definió el problema de sintetizar un circuito a partir de requisitos matemáticos. [2] Aunque el trabajo solo se refiere a circuitos y no a programas, se considera que el trabajo es una de las primeras descripciones de la síntesis de programas y algunos investigadores se refieren a la síntesis de programas como "el problema de la iglesia". En la década de 1960, los investigadores de inteligencia artificial exploraron una idea similar para un "programador automático". [ cita requerida ]
Desde entonces, varias comunidades de investigación consideraron el problema de la síntesis de programas. Los trabajos notables incluyen el enfoque teórico de autómatas de 1969 de Büchi y Landweber , [3] y los trabajos de Manna y Waldinger (c. 1980). El desarrollo de lenguajes de programación modernos de alto nivel también puede entenderse como una forma de síntesis de programas.
El comienzo del siglo XXI ha visto un aumento del interés práctico en la idea de la síntesis de programas en la comunidad de verificación formal y campos relacionados. Armando Solar-Lezama demostró que es posible codificar problemas de síntesis de programas en lógica booleana y usar algoritmos para el problema de satisfacibilidad booleana para encontrar programas automáticamente. [4] En 2013, investigadores de UPenn , UC Berkeley y MIT propusieron un marco unificado para problemas de síntesis de programas . [5]Desde 2014 ha habido una competencia anual de síntesis de programas que compara los diferentes algoritmos para la síntesis de programas en un evento competitivo, la Competencia de síntesis guiada por sintaxis o SyGuS-Comp. [6] Aún así, los algoritmos disponibles solo pueden sintetizar pequeños programas.
El marco de trabajo de Manna y Waldinger , publicado en 1980, [7] [8] parte de una fórmula de especificación de primer orden proporcionada por el usuario . Para esa fórmula, se construye una prueba, sintetizando así también un programa funcional a partir de sustituciones unificadoras .
Inicialmente, el conocimiento previo, las condiciones previas y las condiciones posteriores se ingresan en la tabla. Después de eso, las reglas de prueba apropiadas se aplican manualmente. El marco ha sido diseñado para mejorar la legibilidad humana de las fórmulas intermedias: al contrario de la resolución clásica , no requiere la forma normal de la cláusula , pero permite razonar con fórmulas de estructura arbitraria y que contienen junctores (" resolución sin cláusula "). La prueba está completa cuando se ha derivado en la columna Metas , o, de manera equivalente, en la columna Afirmaciones . Se garantiza que los programas obtenidos por este enfoque satisfagan la fórmula de especificación a partir de la cual se inició; en este sentido soncorrecta por construcción . [9] Solo se admite un lenguaje de programación minimalista, aunque completo de Turing , [10] puramente funcional , que consta de operadores condicionales, recursivos, aritméticos y otros [nota 3] . Los estudios de casos realizados dentro de este marco sintetizaron algoritmos para calcular, por ejemplo , división , resto , [11] raíz cuadrada , [12] unificación de términos , [13] respuestas a consultas de bases de datos relacionales [14] y varios algoritmos de clasificación . [15] [16]
