Síntesis de programas

En informática , la síntesis de programas es la tarea de construir un programa que satisfaga demostrablemente una especificación formal de alto nivel dada . A diferencia de la verificación de programas , el programa debe construirse en lugar de 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]

La principal aplicación de la síntesis de programas es liberar al programador de la carga de escribir código correcto y eficiente que satisfaga una especificación. Sin embargo, la síntesis de programas también tiene aplicaciones en la superoptimización y la inferencia de invariantes de bucles . ^[2]

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. ^[3] Aunque el trabajo solo se refiere a circuitos y no a programas, se considera que 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 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 han considerado el problema de la síntesis de programas. Entre los trabajos más destacados se encuentran el enfoque teórico de autómatas de Büchi y Landweber de 1969 [ 4 ] y ^los trabajos de Manna y Waldinger (c. 1980). El desarrollo de los lenguajes de programación de alto nivel modernos también puede entenderse como una forma de síntesis de programas.

Esta sección necesita una ampliación con una descripción más detallada de los enfoques contemporáneos. Puedes ayudar agregándole algo. ( Diciembre de 2022 )

A principios del siglo XXI, se ha producido un aumento del interés práctico en la idea de la síntesis de programas en la comunidad de verificación formal y en campos relacionados. Armando Solar-Lezama demostró que es posible codificar problemas de síntesis de programas en lógica booleana y utilizar algoritmos para el problema de satisfacibilidad booleana para encontrar programas automáticamente. ^[5]

En 2013, investigadores de la Universidad de Pensilvania , la Universidad de California en Berkeley y el MIT propusieron un marco unificado para los problemas de síntesis de programas denominado Síntesis guiada por sintaxis (SyGuS estilizado) . ^[6] La entrada a un algoritmo SyGuS consiste en una especificación lógica junto con una gramática de expresiones libre de contexto que restringe la sintaxis de las soluciones válidas. ^[7] Por ejemplo, para sintetizar una función f que devuelve el máximo de dos números enteros, la especificación lógica podría verse así:

( f ( x , y ) = x ∨ f ( x , y ) = y ) ∧ f ( x , y ) ≥ x ∧ f ( x , y ) ≥ y

y la gramática podría ser:

< Exp >  ::= x | y | 0 | 1 | < Exp > + < Exp > | ite( < Cond > , < Exp > , < Exp > ) < Cond >  ::=  < Exp > <= < Exp >

donde "ite" significa "si-entonces-sino". La expresión

ite(x <= y, y, x)

sería una solución válida, porque se ajusta a la gramática y a la especificación.

Desde 2014 hasta 2019, la competencia anual de síntesis guiada por sintaxis (o SyGuS-Comp) comparó los diferentes algoritmos para la síntesis de programas en un evento competitivo. ^[8] La competencia utilizó un formato de entrada estandarizado, SyGuS-IF, basado en SMT-Lib 2. Por ejemplo, el siguiente SyGuS-IF codifica el problema de sintetizar el máximo de dos números enteros (como se presentó anteriormente):

(lógica de conjuntos LIA)(sintetizador-diversión f ((x Int) (y Int)) Int ((i Int) (c Int) (b Bool)) ((i Int (cxy (+ ii) (ite bii))) (cInt(0 1)) (b booleano ((<= ii)))))(declarar-var x Int)(declarar-var y Int)(restricción (>= (fxy) x))(restricción (>= (fxy) y))(restricción (o (= (fxy) x) (= (fxy) y)))(verificar sintetizador)

Un solucionador compatible podría devolver el siguiente resultado:

((define-fun f ((x Int) (y Int)) Int (ite (<= xy) yx)))

La síntesis inductiva guiada por contraejemplos (CEGIS) es un enfoque eficaz para construir sintetizadores de programas de sonido. ^{[9] [10]} CEGIS implica la interacción de dos componentes: un generador que genera programas candidatos y un verificador que verifica si los candidatos satisfacen la especificación.

Dado un conjunto de entradas I , un conjunto de programas posibles P y una especificación S , el objetivo de la síntesis de programas es encontrar un programa p en P tal que para todas las entradas i en I , S ( p , i ) se cumpla. CEGIS está parametrizado sobre un generador y un verificador:

• El generador toma un conjunto de entradas T y genera un programa candidato c que es correcto en todas las entradas en T , es decir, un candidato tal que para todas las entradas t en T , S ( c , t ) es válido.
• El verificador toma un programa candidato c y devuelve verdadero si el programa satisface S en todas las entradas, y de lo contrario devuelve un contraejemplo , es decir, una entrada e en I tal que S ( c , e ) falla.

CEGIS ejecuta el generador y el verificador en un bucle, acumulando contraejemplos:

El algoritmo cegis es  la entrada : Generador de programas genera , verificador verificar , especificación especificación , salida : Programa que satisface la especificación , o falla entradas  := conjunto vacío bucle  candidato  := generar ( especificación , entradas ) si  verificar ( especificación , candidato ) entonces  devolver  candidato  de lo contrario  verificar produce un contraejemplo e agregar e a las entradas  fin si

Las implementaciones de CEGIS normalmente utilizan solucionadores SMT como verificadores.

CEGIS se inspiró en el refinamiento de abstracción guiado por contraejemplos (CEGAR). ^[11]

Reglas de resolución no clausulares (no se muestran las sustituciones unificadoras)

Nro.	Afirmaciones	Objetivos	Programa	Origen
51	${\displaystyle E[p]}$
52	${\estilo de visualización F[p]}$
53		${\displaystyle G[p]}$	s
54		${\estilo de visualización H[p]}$	a
55	${\displaystyle E[{\text{verdadero}}]\lo F[{\text{falso}}]}$			Resolver(51,52)
56		${\displaystyle \lno F[{\text{verdadero}}]\land G[{\text{falso}}]}$	s	Resolver(52,53)
57		${\displaystyle \lnot F[{\text{falso}}]\land G[{\text{verdadero}}]}$	s	Resolver(53,52)
58		${\displaystyle G[{\text{verdadero}}]\land H[{\text{falso}}]}$	p ? s : t	Resolver(53,54)

El marco de trabajo de Manna y Waldinger , publicado en 1980, ^{[12] [13]} 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 formato de tabla, cuyas columnas contienen:

• Un número de línea ("Nr") para fines de referencia
• Fórmulas que ya han sido establecidas, incluyendo axiomas y precondiciones ("Afirmaciones")
• Fórmulas aún por demostrar, incluidas las poscondiciones ("Objetivos"), ^{[nota 1]}
• Términos que denotan un valor de salida válido ("Programa") ^{[nota 2]}
• Una justificación para la línea actual ("Origen")

Inicialmente, se introducen en la tabla los conocimientos previos, las precondiciones y las poscondiciones. Después, se aplican manualmente las reglas de prueba adecuadas. 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 una forma normal clausular , pero permite razonar con fórmulas de estructura arbitraria y que contengan cualquier conector (" resolución no clausular "). La prueba está completa cuando se ha derivado en la columna Objetivos o, equivalentemente, en la columna Afirmaciones . Se garantiza que los programas obtenidos mediante este enfoque satisfacen la fórmula de especificación de la que se partió; en este sentido, son correctos por construcción . ^{[14] Solo se admite un} lenguaje de programación minimalista, pero Turing-completo , ^[15] puramente funcional , que consta de operadores condicionales, de recursión y aritméticos y otros ^{[nota 3]} . Los estudios de caso realizados dentro de este marco sintetizaron algoritmos para calcular, por ejemplo, división , resto , ^[16] raíz cuadrada , ^[17] unificación de términos , ^[18] respuestas a consultas de bases de datos relacionales ^[19] y varios algoritmos de ordenamiento . ^{[20] [21]}${\displaystyle {\it {verdadero}}}$${\displaystyle {\it {falso}}}$

Las reglas de prueba incluyen:

• Resolución no clausular (ver tabla).

Por ejemplo, la línea 55 se obtiene resolviendo las fórmulas de aserción de 51 y de 52, que comparten alguna subfórmula común . El resolvente se forma como la disyunción de , con reemplazado por , y , con reemplazado por . Este resolvente se deduce lógicamente de la conjunción de y . De manera más general, y necesitan tener solo dos subfórmulas unificables y , respectivamente; su resolvente 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 . ^[22]${\estilo de visualización E}$${\estilo de visualización F}$${\estilo de visualización p}$${\estilo de visualización E}$${\estilo de visualización p}$${\displaystyle {\it {verdadero}}}$${\estilo de visualización F}$${\estilo de visualización p}$${\displaystyle {\it {falso}}}$${\estilo de visualización E}$${\estilo de visualización F}$${\estilo de visualización E}$${\estilo de visualización F}$$estilo de visualización p_{1}}$$estilo de visualización p_{2}$${\displaystyle E\theta}$${\estilo de visualización F\theta}$${\estilo de visualización \theta}$$estilo de visualización p_{1}}$$estilo de visualización p_{2}$

Los términos del programa de las fórmulas principales se combinan como se muestra en la línea 58 para formar la salida del resolvente. 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 únicamente en subfórmulas correspondientes a propiedades computables .${\estilo de visualización \theta}$${\estilo de visualización p}$

• Transformaciones lógicas.

Por ejemplo, se puede transformar a ) tanto en Afirmaciones como en Metas, ya que ambas son equivalentes.${\displaystyle E\land (F\lor G)}$${\displaystyle (E\land F)\lor (E\land G)}$

• Desdoblamiento de afirmaciones conjuntivas y de objetivos disyuntivos.

Un ejemplo se muestra 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 , encuentre tal que ", y un orden adecuado dado por el usuario del dominio de , siempre es adecuado agregar una Aserción " ". ^[23] Resolver con esta aserción puede introducir una llamada recursiva a en el término del Programa.${\estilo de visualización x}$${\displaystyle {\textit {pre}}(x)}$${\displaystyle f(x)=y}$${\displaystyle {\textit {publicación}}(x,y)}$ ${\estilo de visualización \prec}$${\estilo de visualización x}$${\displaystyle x'\prec x\land {\textit {pre}}(x')\implies {\textit {post}}(x',f(x'))}$${\estilo de visualización f}$

Un ejemplo se da 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 buen orden definido por (p.110).${\displaystyle (n',d')\prec (n,d)}$${\displaystyle 0\leq n'<n}$

Murray ha demostrado que estas reglas son completas para la lógica de primer orden . ^[24] En 1986, Manna y Waldinger agregaron reglas generalizadas de E-resolución y paramodulación para manejar también la igualdad; ^[25] más tarde, estas reglas resultaron ser incompletas (pero sin embargo sólidas ). ^[26]

Ejemplo de síntesis de función máxima

Nro.	Afirmaciones	Objetivos	Programa	Origen
1	${\displaystyle A=A}$			Axioma
2	${\estilo de visualización A\leq A}$			Axioma
3	${\displaystyle A\leq B\lor B\leq A}$			Axioma
10		${\displaystyle x\leq M\land y\leq M\land (x=M\lor y=M)}$	METRO	Especificación
11		${\displaystyle (x\leq M\land y\leq M\land x=M)\lor (x\leq M\land y\leq M\land y=M)}$	METRO	Distribucion(10)
12		${\displaystyle x\leq M\land y\leq M\land x=M}$	METRO	Dividir(11)
13		${\displaystyle x\leq M\land y\leq M\land y=M}$	METRO	Dividir(11)
14		${\displaystyle x\leq x\land y\leq x}$	incógnita	Resolver(12,1)
15		${\displaystyle y\leq x}$	incógnita	Resolver(14,2)
16		${\displaystyle \lno(x\leq y)}$	incógnita	Resolver(15,3)
17		${\displaystyle x\leq y\land y\leq y}$	y	Resolver(13,1)
18		${\displaystyle x\leq y}$	y	Resolver(17,2)
19		${\displaystyle {\textit {verdadero}}}$	x<y ? y : x	Resolver(18,16)

Como ejemplo de juguete, un programa funcional para calcular el máximo de dos números se puede derivar de la siguiente manera. ^{[ cita requerida ]}${\estilo de visualización M}$${\estilo de visualización x}$${\estilo de visualización y}$

Partiendo 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 ", se obtiene la fórmula de primer orden como su traducción formal. Esta fórmula se debe demostrar. Mediante la Skolemización inversa , ^{[nota 4]} se obtiene la especificación de la línea 10, una letra mayúscula y una minúscula que denotan una variable y una constante de Skolem , respectivamente.${\displaystyle \para todo X\para todo Y\existe M:X\leq M\land Y\leq M\land (X=M\lor Y=M)}$

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, las líneas 12 y 13.

Volviendo al primer caso, resolver la línea 12 con el axioma de la línea 1 conduce a la instanciación de la variable de programa en la línea 14. Intuitivamente, el último conjuntivo de la línea 12 prescribe el valor que debe tomar en este caso. Formalmente, la regla de resolución no clausular que se muestra en la línea 57 anterior se aplica a las líneas 12 y 1, con ${\estilo de visualización M}$${\estilo de visualización M}$

• siendo p la instancia común x=x de A=A y x=M , obtenida unificando sintácticamentelas últimas fórmulas,
• F[ p ] siendo verdadero ∧ x=x , obtenido de la línea instanciada 1 (rellenada apropiadamente para hacer visible el contexto F[⋅] alrededor de p ), y
• G[ p ] siendo x ≤ x ∧ y ≤ x ∧ x = x , obtenido de la línea instanciada 12,

produciendo verdadero ∧ falso ) ∧ ( x ≤ x ∧ y ≤ x ∧ verdadero , lo que se simplifica a .${\displaystyle \lno (}$${\estilo de visualización )}$${\displaystyle x\leq x\land y\leq x}$

De manera similar, la línea 14 genera la línea 15 y luego la línea 16 por resolución. Asimismo, el segundo caso, en la línea 13, se maneja de manera similar y finalmente genera la línea 18.${\displaystyle x\leq M\land y\leq M\land y=M}$

En un último paso, ambos casos (es decir, las líneas 16 y 18) se unen, utilizando la regla de resolución de la línea 58; para que esa regla sea aplicable, se necesitó el paso preparatorio 15→16. Intuitivamente, la línea 18 podría leerse como "en caso de que , la salida sea válida (con respecto a la especificación original), mientras que la línea 15 dice "en caso de que , la salida sea válida; 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 de programa. Dado que se ha derivado la fórmula del objetivo , la prueba está hecha y la columna de programa de la línea " " contiene el programa.${\displaystyle x\leq y}$${\estilo de visualización y}$${\displaystyle y\leq x}$${\estilo de visualización x}$${\displaystyle {\textit {verdadero}}}$${\displaystyle {\textit {verdadero}}}$

• Programación inductiva
• Metaprogramación
• Derivación de programas
• Programación en lenguaje natural
• Síntesis reactiva

• David, Cristina; Kroening, Daniel (13 de octubre de 2017). "Síntesis del programa: retos y oportunidades". Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences . 375 (2104): 20150403. doi :10.1098/rsta.2015.0403. ISSN  1364-503X. PMC  5597726 . PMID  28871052.
• Alur, Rajeev; Singh, Rishabh; Fisman, Dana; Solar-Lezama, Armando (2018-11-20). "Síntesis de programas basada en búsqueda". Comunicaciones de la ACM . 61 (12): 84–93. doi :10.1145/3208071. ISSN  0001-0782.
• Zohar Manna, Richard Waldinger (1975). "Conocimiento y razonamiento en la síntesis de programas". Inteligencia artificial . 6 (2): 175–208. doi :10.1016/0004-3702(75)90008-9.
• Solar-Lezama, Armando (2008). Síntesis de programas mediante croquis (PDF) (Ph.D.). Universidad de California, Berkeley.