En informática , la síntesis de programas es la tarea de construir un programa que satisfaga de manera demostrable una especificación formal de alto nivel dada . A diferencia de la verificación del programa, el programa debe construirse en lugar de darse; sin embargo, ambos campos hacen uso de técnicas de prueba formales y ambos comprenden enfoques de diferentes grados de automatización. En contraste con las técnicas de programación automática , las especificaciones en la síntesis de programas son generalmente declaraciones no algorítmicas en un cálculo lógico apropiado . [1]
Origen
Durante el Instituto de Verano de Lógica Simbólica en la Universidad de Cornell en 1957, Alonzo Church definió el problema para 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 es una de las primeras descripciones de síntesis de programas y algunos investigadores se refieren a la síntesis de programas como "Problema de Church". En la década de 1960, los investigadores en 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 los 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.
Desarrollos del siglo XXI
El comienzo del siglo XXI ha sido testigo de un aumento del interés práctico en la idea de 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 booleano 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 un concurso anual de síntesis de programas que compara los diferentes algoritmos para la síntesis de programas en un evento competitivo, el Concurso de síntesis guiada por sintaxis o SyGuS-Comp. [6] Aún así, los algoritmos disponibles solo pueden sintetizar programas pequeños.
Un artículo de 2015 demostró que la síntesis de programas PHP ha demostrado axiomáticamente que cumplen con una especificación determinada, con fines tales como verificar que un número sea primo o enumerar los factores de un número. [7]
El marco de Manna y Waldinger
Nr | Afirmaciones | Metas | Programa | Origen |
---|---|---|---|---|
51 | ||||
52 | ||||
53 | s | |||
54 | t | |||
55 | Resolver (51,52) | |||
56 | s | Resolver (52,53) | ||
57 | s | Resolver (53,52) | ||
58 | p ? s : t | Resolver (53,54) |
El marco de Manna y Waldinger , publicado en 1980, [8] [9] parte de una fórmula de especificación de primer orden dada por el usuario . Para esa fórmula, se construye una prueba, sintetizando así también un programa funcional a partir de sustituciones unificadoras .
El marco se presenta en un diseño de tabla, las columnas contienen:
- Un número de línea ("Nr") para fines de referencia
- Fórmulas que ya se han establecido, incluidos axiomas y condiciones previas ("afirmaciones")
- Fórmulas aún por probar, incluidas las condiciones posteriores ("Objetivos"), [nota 1]
- Términos que denotan un valor de salida válido ("Programa") [nota 2]
- Una justificación de la línea actual ("Origen")
Inicialmente, los conocimientos previos, 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 fórmulas intermedias: contrariamente a la resolución clásica , no requiere forma normal clausal , pero permite razonar con fórmulas de estructura arbitraria y que contienen cualquier unión (" resolución no clausal "). La prueba está completa cuandose ha derivado en la columna Objetivos o, de forma equivalente,en la columna Afirmaciones . Se garantiza que los programas obtenidos mediante este enfoque satisfacen la fórmula de especificación a partir de la cual en este sentido son correctos por construcción . [10] Sólo un minimalista, sin embargo, Turing completo , lenguaje de programación funcional , que consiste en condicional, recursividad, y los operadores aritméticos y otros [nota 3] es compatible. Los estudios de caso 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]
Reglas de prueba
Las reglas de prueba incluyen:
- Resolución no clausal (ver tabla).
- Por ejemplo, la línea 55 se obtiene resolviendo fórmulas de afirmación desde 51 y de 52 que comparten alguna subfórmula común . El resolutivo se forma como la disyunción de , con reemplazado por , y , con reemplazado por . Este resolutivo se sigue lógicamente de la conjunción de y . Más generalmente, y necesita tener solo dos subfórmulas unificables y , respectivamente; su resolutivo se forma entonces a partir de y como antes, donde es el unificador más general de y . Esta regla generaliza la resolución de cláusulas . [17]
- Los términos del programa de las fórmulas principales se combinan como se muestra en la línea 58 para formar el resultado del resolutivo. En el caso general, se aplica también a este último. Dado que la subfórmula aparece en la salida, se debe tener cuidado de resolver solo en subfórmulas correspondientes a propiedades computables .
- Transformaciones lógicas.
- Por ejemplo, se puede transformar en ) tanto en Afirmaciones como en Metas, ya que ambas son equivalentes.
- Escisión de afirmaciones conjuntivas y de metas disyuntivas.
- Se muestra un ejemplo en las líneas 11 a 13 del ejemplo de juguete a continuación.
- Inducción estructural .
- Esta regla permite la síntesis de funciones recursivas . Para una condición previa y posterior dada "Dado tal que , encontrar tal que ", y una ordenación adecuada proporcionada por el usuario del dominio de , siempre es correcto agregar una afirmación " ". [18] Resolver con esta afirmación puede introducir una llamada recursiva a en el plazo del programa.
- Se da un ejemplo en Manna, Waldinger (1980), p. 108-111, donde se sintetiza un algoritmo para calcular el cociente y el resto de dos números enteros dados, utilizando el orden de pozo definido por (pág.110).
Murray ha demostrado que estas reglas son completas para la lógica de primer orden . [19] En 1986, Manna y Waldinger agregaron reglas de paramodulación y resolución electrónica generalizadas para manejar también la igualdad; [20] más tarde, estas reglas resultaron ser incompletas (pero no obstante sólidas ). [21]
Ejemplo
Nr | Afirmaciones | Metas | Programa | Origen |
---|---|---|---|---|
1 | Axioma | |||
2 | Axioma | |||
3 | Axioma | |||
10 | METRO | Especificación | ||
11 | METRO | Distr (10) | ||
12 | METRO | Separado (11) | ||
13 | METRO | Separado (11) | ||
14 | X | Resolver (12,1) | ||
15 | X | Resolver (14,2) | ||
dieciséis | X | Resolver (15,3) | ||
17 | y | Resolver (13,1) | ||
18 | y | Resolver (17,2) | ||
19 | x | Resolver (18,16) |
Como ejemplo de juguete, un programa funcional para calcular el máximo de dos números y se puede derivar de la siguiente manera. [ cita requerida ]
A partir de la descripción del requisito " El máximo es mayor o igual que cualquier número dado, y es uno de los números dados ", la fórmula de primer ordense obtiene como su traducción formal. Esta fórmula debe probarse. Por skolemización inversa , [nota 4] se obtiene la especificación en la línea 10, una letra mayúscula y minúscula que denota una variable y una constante de Skolem , respectivamente.
Después de aplicar una regla de transformación para la ley distributiva en la línea 11, el objetivo de la prueba es una disyunción y, por lo tanto, se puede dividir en dos casos, a saber. líneas 12 y 13.
Pasando al primer caso, resolver la línea 12 con el axioma en la línea 1 conduce a la instanciación de la variable de programa en la línea 14. Intuitivamente, la última conjunción de la línea 12 prescribe el valor que debe tomar en este caso. Formalmente, la regla de resolución no cláusula que se muestra en la línea 57 anterior se aplica a las líneas 12 y 1, con
- siendo p la instancia común x = x de A = A y x = M , obtenida unificando sintácticamentelas últimas fórmulas,
- F [ p ] siendo cierto ∧ x = x , obtenido de lalínea instanciada 1 (debidamente rellenada para hacervisibleel contexto F [⋅] alrededor de p ), y
- G [ p ] siendo x ≤ x ∧ y ≤ x ∧ x = x , obtenido de la línea 12 instanciada,
flexible verdadero ∧ falso ) ∧ ( x ≤ x ∧ y ≤ x ∧ verdadero, que simplifica a .
De manera similar, la línea 14 produce la línea 15 y luego la línea 16 por resolución. Además, el segundo caso, en la línea 13, se maneja de manera similar, produciendo finalmente la línea 18.
En un último paso, se unen ambos casos (es decir, las líneas 16 y 18), utilizando la regla de resolución de la línea 58; para que esa regla fuera aplicable, se necesitaba el paso preparatorio 15 → 16. Intuitivamente, la línea 18 podría leerse como "en caso, La salida es válido (con respecto a la especificación original), mientras que la línea 15 dice "en caso de , La salida es válido; el paso 15 → 16 estableció que ambos casos 16 y 18 son complementarios. [nota 5] Dado que tanto la línea 16 como la 18 vienen con un término de programa, una expresión condicional da como resultado la columna del programa. Desde la fórmula de la meta se ha derivado, la prueba está hecha y la columna del programa del ""La línea contiene el programa.
Este procedimiento produce un solo operador de la forma p? S: t tomado de la línea 58. Este no es un lenguaje de programación porque no es Turing Complete. No hay comandos, por ejemplo, ASSIGNMENT, IF / ELSE, FOR / WHILE o programas recursivos, que sean necesarios para hacer que un lenguaje sea Turing Complete. Debería etiquetarse como tal: una forma de crear un único operador lógico, no una forma de crear programas en general. Quizás se podría utilizar la “síntesis del operador”. Un método para construir una rueda no es un método para construir un automóvil. [ cita requerida ]
Ver también
- Programación inductiva
- Metaprogramación
- Programacion automatica
- Derivación del programa
- Programación en lenguaje natural
- Síntesis reactiva
- Verificación formal
Notas
- ^ La distinción "Afirmaciones" / "Metas" es solo por conveniencia; siguiendo el paradigma de la prueba por contradicción , una Meta es equivalente a una aserción .
- ^ Cuando y es la fórmula de la meta y el término del programa en una línea, respectivamente, entonces en todos los casos donde sostiene, es una salida válida del programa a sintetizar. Este invariante es mantenido por todas las reglas de prueba. Por lo general, una fórmula de afirmación no está asociada con un término del programa.
- ^ Solo el operador condicional ( ?:) Es compatible desde el principio. Sin embargo, se pueden agregar nuevos operadores y relaciones arbitrarios proporcionando sus propiedades como axiomas. En el ejemplo de juguete a continuación, solo las propiedades de y que son realmente necesarios en la demostración se han axiomatizado, en la línea 1 a 3.
- ^ Mientras que la skolemización ordinaria conserva la satisfacibilidad, la skolemización inversa, es decir, la sustitución de variables cuantificadas universalmente por funciones, conserva la validez.
- ^ Para eso se necesitaba el Axioma 3; de hecho, sino era un pedido total , no se pudo calcular un máximo para entradas incomparables.
Referencias
- ^ Cuenca, D .; Deville, Y .; Flener, P .; Hamfelt, A .; Fischer Nilsson, J. (2004). "Síntesis de programas en lógica computacional". En M. Bruynooghe y K.-K. Lau (ed.). Desarrollo de programas en lógica computacional . LNCS. 3049 . Saltador. págs. 30–65. CiteSeerX 10.1.1.62.4976 .
- ^ Iglesia de Alonzo (1957). "Aplicaciones de la aritmética recursiva al problema de la síntesis de circuitos". Resúmenes del Instituto de Verano de Lógica Simbólica . 1 : 3–50.
- ^ Richard Büchi, Lawrence Landweber (abril de 1969). "Resolución de condiciones secuenciales mediante estrategias de estados finitos" . Transacciones de la American Mathematical Society . 138 : 295–311. doi : 10.2307 / 1994916 . JSTOR 1994916 .
- ^ Solar-Lezama, Armando (2008). Programa de síntesis mediante bocetos (Ph.D.). Universidad de California, Berkeley.
- ^ Alur, Rajeev; al., et. (2013). "Síntesis guiada por sintaxis". Actas de métodos formales en diseño asistido por computadora . IEEE. pag. 8.
- ^ SyGuS-Comp (Competencia de síntesis guiada por sintaxis)
- ^ Charles Volkstorf (7 de enero de 2015). "Programa de síntesis de prueba axiomática de corrección". arXiv : 1501.01363 [ cs.LO ].
- ^ Zohar Manna, Richard Waldinger (enero de 1980). "Un enfoque deductivo de la síntesis del programa". Transacciones ACM sobre lenguajes y sistemas de programación . 2 : 90-121. doi : 10.1145 / 357084.357090 .
- ^ Zohar Manna y Richard Waldinger (diciembre de 1978). Un enfoque deductivo de la síntesis del programa (PDF) (Nota técnica). SRI Internacional.
- ↑ Ver Manna, Waldinger (1980), p.100 para conocer la exactitud de las reglas de resolución.
- ↑ Manna, Waldinger (1980), p. 108-111.
- ^ Zohar Manna y Richard Waldinger (agosto de 1987). "El origen de un paradigma de búsqueda binaria" . Ciencia de la Programación de Computadores . 9 (1): 37–83. doi : 10.1016 / 0167-6423 (87) 90025-6 .
- ^ Daniele Nardi (1989). "Síntesis formal de un algoritmo de unificación por el método deductivo-tablero" . Revista de programación lógica . 7 : 1–43. doi : 10.1016 / 0743-1066 (89) 90008-3 .
- ^ Daniele Nardi y Riccardo Rosati (1992). "Síntesis deductiva de programas de respuesta a consultas". En Kung-Kiu Lau y Tim Clement (ed.). Taller Internacional de Síntesis y Transformación de Programas Lógicos (LOPSTR) . Talleres de Informática. Saltador. págs. 15-29. doi : 10.1007 / 978-1-4471-3560-9_2 .
- ^ Jonathan Traugott (1986). "Síntesis deductiva de programas de clasificación". Actas de la Conferencia Internacional sobre Deducción Automatizada . LNCS . 230 . Saltador. págs. 641–660.
- ^ Jonathan Traugott (junio de 1989). "Síntesis deductiva de programas de clasificación" . Revista de Computación Simbólica . 7 (6): 533–572. doi : 10.1016 / S0747-7171 (89) 80040-9 .
- ↑ Manna, Waldinger (1980), p. 99
- ↑ Manna, Waldinger (1980), p. 104
- ↑ Manna, Waldinger (1980), p.103, refiriéndose a: Neil V. Murray (febrero de 1979). Un procedimiento de prueba para la lógica de primer orden no clausal libre de cuantificadores (informe técnico). Univ. De Syracuse 2-79.
- ^ Zohar Manna, Richard Waldinger (enero de 1986). "Relaciones especiales en la deducción automatizada". Revista de la ACM . 33 : 1-59. doi : 10.1145 / 4904.4905 .
- ^ Zohar Manna, Richard Waldinger (1992). "Las reglas de relaciones especiales están incompletas". Proc. CADE 11 . LNCS. 607 . Saltador. págs. 492–506.
- Zohar Manna, Richard Waldinger (1975). "Conocimiento y razonamiento en síntesis de programas". Inteligencia artificial . 6 (2): 175–208. doi : 10.1016 / 0004-3702 (75) 90008-9 .
- Jonathan Traugott (1986). "Síntesis deductiva de programas de clasificación". Actas de la Conferencia Internacional sobre Deducción Automatizada . LNCS. 230 . Saltador. págs. 641–660.