Hispanopedia Wiki
Articulo de referencia

Interpretación abstracta

En informática , la interpretación abstracta es una teoría de aproximación sólida de la semántica de los programas informáticos , basada en funciones monótonas sobre conjuntos o...

Hispanopedia WikiContenido en espanolLectura gratuita

En informática , la interpretación abstracta es una teoría de aproximación sólida de la semántica de los programas informáticos , basada en funciones monótonas sobre conjuntos ordenados , especialmente retículos . Puede considerarse como una ejecución parcial de un programa informático que obtiene información sobre su semántica (por ejemplo, flujo de control , flujo de datos ) sin realizar todos los cálculos .

Su principal aplicación concreta es el análisis estático formal , la extracción automática de información sobre las posibles ejecuciones de programas informáticos; dichos análisis tienen dos usos principales:

La interpretación abstracta fue formalizada por la pareja de científicos informáticos franceses Patrick Cousot y Radhia Cousot a finales de la década de 1970. [ 1 ] [ 2 ]

Intuición

Esta sección ilustra la interpretación abstracta mediante ejemplos del mundo real, ajenos al ámbito de la informática.

Consideremos a las personas presentes en una sala de conferencias. Supongamos que cada persona tiene un identificador único, como el número de la seguridad social en Estados Unidos. Para comprobar la ausencia de alguien, basta con verificar si su número de la seguridad social figura en la lista. Dado que dos personas distintas no pueden tener el mismo número, es posible confirmar o desmentir la presencia de un participante simplemente consultando su número.

Sin embargo, es posible que solo se hayan registrado los nombres de los asistentes. Si el nombre de una persona no aparece en la lista, podemos concluir con seguridad que no estuvo presente; pero si aparece, no podemos concluirlo definitivamente sin más averiguaciones, debido a la posibilidad de homónimos (por ejemplo, dos personas llamadas John Smith). Cabe señalar que esta información imprecisa seguirá siendo suficiente para la mayoría de los propósitos, ya que los homónimos son poco frecuentes en la práctica. Sin embargo, con todo rigor, no podemos afirmar con certeza que alguien estuviera presente en la sala; lo único que podemos decir es que posiblemente estuvo allí. Si la persona que buscamos es un delincuente, daremos la alarma ; pero, por supuesto, existe la posibilidad de dar una falsa alarma . Fenómenos similares ocurrirán en el análisis de programas.

Si solo nos interesa alguna información específica, por ejemplo, "¿había una persona de edad?"norte{\displaystyle n}¿en la habitación?, mantener una lista de todos los nombres y fechas de nacimiento es innecesario. Podemos restringirnos de forma segura y sin pérdida de precisión a mantener una lista de las edades de los participantes. Si esto ya es demasiado para manejar, podríamos mantener solo la edad del más joven,metro{\displaystyle m}y la persona de mayor edad,METRO{\displaystyle M}Si la pregunta se refiere a una edad estrictamente inferior ametro{\displaystyle m}o estrictamente superior aMETRO{\displaystyle M}En ese caso, podemos afirmar con seguridad que no había ningún participante presente. De lo contrario, solo podremos decir que no lo sabemos.

En el ámbito de la informática, la información concreta y precisa generalmente no se puede calcular en un tiempo y memoria finitos (véase el teorema de Rice y el problema de la parada ). La abstracción se utiliza para permitir respuestas generalizadas a las preguntas (por ejemplo, responder "quizás" a una pregunta de sí o no, es decir, "sí o no", cuando nosotros (un algoritmo de interpretación abstracta) no podemos calcular la respuesta precisa con certeza); esto simplifica los problemas, haciéndolos susceptibles de soluciones automáticas. Un requisito fundamental es añadir suficiente vaguedad para que los problemas sean manejables, manteniendo al mismo tiempo la precisión necesaria para responder a las preguntas importantes (como "¿podría fallar el programa?").

Interpretación abstracta de programas informáticos

Dado un lenguaje de programación o de especificación, la interpretación abstracta consiste en proporcionar varias semánticas vinculadas por relaciones de abstracción. Una semántica es una caracterización matemática de un posible comportamiento del programa. Las semánticas más precisas, que describen con gran exactitud la ejecución real del programa, se denominan semánticas concretas . Por ejemplo, la semántica concreta de un lenguaje de programación imperativo puede asociar a cada programa el conjunto de trazas de ejecución que puede producir ; una traza de ejecución es una secuencia de posibles estados consecutivos de la ejecución del programa; un estado generalmente consta del valor del contador de programa y las ubicaciones de memoria (globales, pila y montón). A continuación, se derivan semánticas más abstractas; por ejemplo, se puede considerar únicamente el conjunto de estados alcanzables en las ejecuciones (lo que equivale a considerar los últimos estados en trazas finitas).

El objetivo del análisis estático es obtener una interpretación semántica computable en algún punto. Por ejemplo, se puede optar por representar el estado de un programa que manipula variables enteras omitiendo los valores reales de las variables y conservando únicamente sus signos (+, − o 0). Para algunas operaciones elementales, como la multiplicación , esta abstracción no pierde precisión: para obtener el signo de un producto, basta con conocer el signo de los operandos. Para otras operaciones, la abstracción puede perder precisión: por ejemplo, es imposible conocer el signo de una suma cuyos operandos son respectivamente positivo y negativo.

En ocasiones, es necesario sacrificar precisión para que la semántica sea decidible (véase el teorema de Rice y el problema de la parada ). En general, existe un compromiso entre la precisión del análisis y su decidibilidad ( computabilidad ) o tratabilidad ( coste computacional ).

En la práctica, las abstracciones que se definen se adaptan tanto a las propiedades del programa que se desean analizar como al conjunto de programas objetivo. El primer análisis automatizado a gran escala de programas informáticos con interpretación abstracta fue motivado por el accidente que provocó la destrucción del primer vuelo del cohete Ariane 5 en 1996. [ 3 ]

Formalización

Ejemplo: abstracción de conjuntos de enteros (rojo) a conjuntos de signos (verde)

DejarL{\displaystyle L}Sea un conjunto ordenado , llamado conjunto concreto , y dejemos queL′{\displaystyle L'}sea ​​otro conjunto ordenado, llamado conjunto abstracto . Estos dos conjuntos están relacionados entre sí mediante la definición de funciones totales que asignan elementos de uno al otro.

Una funciónα{\displaystyle \alpha }Se denomina función de abstracción si asigna un elementoincógnita{\displaystyle x}en el conjunto de hormigónL{\displaystyle L}a un elementoα(incógnita){\displaystyle \alpha (x)}en el conjunto abstractoL′{\displaystyle L'}. Es decir, elemento α(incógnita){\displaystyle \alpha (x)}enL′{\displaystyle L'}es la abstracción deincógnita{\displaystyle x}enL{\displaystyle L}.

Una funciónγ{\displaystyle \gamma }Se denomina función de concreción si asigna un elementoincógnita′{\displaystyle x'}en el conjunto abstractoL′{\displaystyle L'}a un elementoγ(incógnita′){\displaystyle \gamma (x')}en el conjunto de hormigónL{\displaystyle L}. Es decir, elementoγ(incógnita′){\displaystyle \gamma (x')}enL{\displaystyle L}es una concreción deincógnita′{\displaystyle x'}enL′{\displaystyle L'}.

DejarL1{\displaystyle L_{1}},L2{\displaystyle L_{2}},L1′{\displaystyle L'_{1}}, yL2′{\displaystyle L'_{2}}ser conjuntos ordenados. La semántica concretaF{\displaystyle f}es una función monótona deL1{\displaystyle L_{1}}aL2{\displaystyle L_{2}}. Una funciónF′{\displaystyle f'}deL1′{\displaystyle L'_{1}}aL2′{\displaystyle L'_{2}}Se dice que es una abstracción válida deF{\displaystyle f}si, para todosincógnita′{\displaystyle x'}enL1′{\displaystyle L'_{1}}, tenemos(F∘γ)(incógnita′)≤(γ∘F′)(incógnita′){\displaystyle (f\circ \gamma )(x')\leq (\gamma \circ f')(x')}.

La semántica de los programas se describe generalmente mediante puntos fijos en presencia de bucles o procedimientos recursivos. Supongamos queL{\displaystyle L}es un retículo completo y deje queF{\displaystyle f}sea ​​una función monótona deL{\displaystyle L}enL{\displaystyle L}. Entonces, cualquierincógnita′{\displaystyle x'}de tal manera queF(incógnita′)≤incógnita′{\displaystyle f(x')\leq x'}es una abstracción del punto fijo más pequeño deF{\displaystyle f}, que existe, según el teorema de Knaster-Tarski .

La dificultad ahora radica en obtener talincógnita′{\displaystyle x'}. SiL′{\displaystyle L'}es de altura finita, o al menos verifica la condición de cadena ascendente (todas las secuencias ascendentes son finalmente estacionarias), entonces talincógnita′{\displaystyle x'}puede obtenerse como el límite estacionario de la secuencia ascendenteincógnitanorte′{\displaystyle x'_{n}}definido por inducción de la siguiente manera:incógnita0′=⊥{\displaystyle x'_{0}=\bot }(el elemento más pequeño deL′{\displaystyle L'}) yincógnitanorte+1′=F′(incógnitanorte′){\displaystyle x'_{n+1}=f'(x'_{n})}.

En otros casos, todavía es posible obtener talincógnita′{\displaystyle x'}a través de un operador de ensanchamiento (de pares) , [ 4 ] definido como un operador binario∇:L×L→L{\displaystyle \nabla \dos puntos L\times L\to L}que cumpla las siguientes condiciones:

  1. A pesar deincógnita{\displaystyle x}yy{\displaystyle y}, tenemosincógnita≤incógnita∇y{\displaystyle x\leq x\mathbin {\nabla } y}yy≤incógnita∇y{\displaystyle y\leq x\mathbin {\nabla } y}, y
  2. Para cualquier secuencia ascendente(ynorte′)norte≥0{\displaystyle (y'_{n})_{n\geq 0}}, la secuencia definida porincógnita0′:=⊥{\displaystyle x'_{0}:=\bot }yincógnitanorte+1′:=incógnitanorte′∇ynorte′{\displaystyle x'_{n+1}:=x'_{n}\mathbin {\nabla } y'_{n}}en última instancia es estacionario. Entonces podemos tomarynorte′=F′(incógnitanorte′){\displaystyle y'_{n}=f'(x'_{n})}.

En algunos casos, es posible definir abstracciones utilizando conexiones de Galois.(α,γ){\displaystyle (\alpha,\gamma)}dóndeα{\displaystyle \alpha }es deL{\displaystyle L}aL′{\displaystyle L'}yγ{\displaystyle \gamma }es deL′{\displaystyle L'}aL{\displaystyle L}Esto supone la existencia de abstracciones óptimas, lo cual no es necesariamente cierto. Por ejemplo, si abstraemos conjuntos de parejas(incógnita,y){\displaystyle (x,y)}de números reales al encerrar poliedros convexos , no hay una abstracción óptima al disco definido porincógnita2+y2≤1{\displaystyle x^{2}+y^{2}\leq 1}.

Ejemplos de dominios abstractos

Dominios abstractos numéricos

Se puede asignar a cada variableincógnita{\displaystyle x}disponible en un punto de programa determinado un intervalo[Lincógnita,Hincógnita]{\displaystyle [L_{x},H_{x}]}. Un estado que asigna el valorv(incógnita){\displaystyle v(x)}a variableincógnita{\displaystyle x}será una concreción de estos intervalos si, para todosincógnita{\displaystyle x}, tenemosv(incógnita)∈[Lincógnita,Hincógnita]{\displaystyle v(x)\in [L_{x},H_{x}]}. Desde los intervalos[Lincógnita,Hincógnita]{\displaystyle [L_{x},H_{x}]}y[Ly,Hy]{\displaystyle [L_{y},H_{y}]}para variablesincógnita{\displaystyle x}yy{\displaystyle y}, respectivamente, se pueden obtener fácilmente intervalos paraincógnita+y{\displaystyle x+y}(a saber,[Lincógnita+Ly,Hincógnita+Hy]{\displaystyle [L_{x}+L_{y},H_{x}+H_{y}]}) y paraincógnita−y{\displaystyle xy}(a saber,[Lincógnita−Hy,Hincógnita−Ly]{\displaystyle [L_{x}-H_{y},H_{x}-L_{y}]}); tenga en cuenta que estas son abstracciones exactas , ya que el conjunto de resultados posibles para, por ejemplo,incógnita+y{\displaystyle x+y}, es precisamente el intervalo[Lincógnita+Ly,Hincógnita+Hy]{\displaystyle [L_{x}+L_{y},H_{x}+H_{y}]}Se pueden derivar fórmulas más complejas para la multiplicación, la división, etc., dando lugar a la denominada aritmética de intervalos . [ 5 ]

Consideremos ahora el siguiente programa muy sencillo:

y = x; z = x - y;

Con tipos aritméticos razonables, el resultado parazdebería ser cero. Pero si hacemos aritmética de intervalos comenzando desdeincógnitaen [0, 1], se obtienezen [−1, +1]. Si bien cada una de las operaciones tomadas individualmente fue abstraída exactamente, su composición no lo es.

El problema es evidente: no hicimos un seguimiento de la relación de igualdad entreincógnitayyEn realidad, este dominio de intervalos no tiene en cuenta ninguna relación entre variables y, por lo tanto, es un dominio no relacional . Los dominios no relacionales suelen ser rápidos y sencillos de implementar, pero imprecisos.

Algunos ejemplos de dominios abstractos numéricos relacionales son:

y combinaciones de los mismos (como el producto reducido, [ 2 ] cf. imagen de la derecha).

Cuando se elige un dominio abstracto, normalmente hay que encontrar un equilibrio entre mantener relaciones detalladas y los altos costes computacionales.

dominios abstractos de palabras de máquina

Mientras que los lenguajes de alto nivel como Python o Haskell utilizan enteros ilimitados por defecto, los lenguajes de programación de bajo nivel como C o el lenguaje ensamblador suelen operar con palabras de máquina de tamaño finito , que se modelan de forma más adecuada utilizando los enteros módulo2norte{\textstyle 2^{n}}(donde n es el ancho de bits de una palabra de máquina). Existen varios dominios abstractos adecuados para diversos análisis de dichas variables.

El dominio del campo de bits trata cada bit en una palabra de máquina por separado, es decir, una palabra de ancho n se trata como una matriz de n valores abstractos. Los valores abstractos se toman del conjunto{0,1,⊥}{\textstyle \{0,1,\bot \}}y las funciones de abstracción y concreción vienen dadas por: [ 14 ] [ 15 ]γ(0)={0}{\displaystyle \gamma (0)=\{0\}},γ(1)={1}{\displaystyle \gamma (1)=\{1\}},γ(⊥)={0,1}{\displaystyle \gamma (\bot )=\{0,1\}},α({0})=0{\displaystyle \alpha (\{0\})=0},α({1})=1{\displaystyle \alpha (\{1\})=1},α({0,1})=⊥{\displaystyle \alpha (\{0,1\})=\bot },α({})=⊥{\displaystyle \alpha (\{\})=\bot }Las operaciones bit a bit sobre estos valores abstractos son idénticas a las operaciones lógicas correspondientes en algunas lógicas trivalentes : [ 16 ]

Otros dominios incluyen el dominio de intervalos con signo y el dominio de intervalos sin signo . Estos tres dominios admiten operadores abstractos hacia adelante y hacia atrás para operaciones comunes como suma, desplazamientos , XOR y multiplicación. Estos dominios se pueden combinar utilizando el producto reducido. [ 17 ]

Véase también

Referencias

  1. ↑ Cousot, Patrick; Cousot, Radhia (1977). "Interpretación abstracta: un modelo reticular unificado para el análisis estático de programas mediante la construcción o aproximación de puntos fijos" (PDF) . Actas del Cuarto Simposio ACM sobre Principios de Lenguajes de Programación, Los Ángeles, California, EE. UU., enero de 1977. ACM Press. págs. 238–252 . doi : 10.1145/512950.512973 . S2CID 207614632 .  
  2. 1 2 Cousot, Patrick; Cousot, Radhia (1979). "Diseño sistemático de marcos de análisis de programas" (PDF) . Actas del sexto simposio anual de la ACM sobre principios de lenguajes de programación, San Antonio, Texas, EE. UU., enero de 1979. ACM Press. págs. 269–282 . doi : 10.1145/567752.567778 . S2CID 1547466 .  
  3. ↑ Faure, Christèle. "Historia de PolySpace Technologies" . Consultado el 3 de octubre de 2010 .
  4. ↑ Cousot, P.; Cousot, R. (agosto de 1992). «Comparación de la conexión de Galois y los enfoques de ampliación/estrechamiento de la interpretación abstracta» (PDF) . En Bruynooghe, Maurice; Wirsing, Martin (eds.). Actas del 4.º Simposio Internacional sobre Implementación de Lenguajes de Programación y Programación Lógica (PLILP) . Lecture Notes in Computer Science. Vol. 631. Springer. págs. 269–296 . ISBN   978-0-387-55844-8.
  5. ↑ Cousot, Patrick; Cousot, Radhia (1976). "Determinación estática de propiedades dinámicas de programas" (PDF) . Actas del Segundo Simposio Internacional sobre Programación . Dunod, París, Francia. pp. 106–130 . 
  6. ↑ Granger, Philippe (1989). "Análisis estático de congruencias aritméticas". International Journal of Computer Mathematics . 30 ( 3–4 ): 165–190 . doi : 10.1080/00207168908803778 .
  7. ↑ Philippe Granger (1991). "Análisis estático de igualdades de congruencia lineal entre variables de un programa". En Abramsky, S.; Maibaum, TSE (eds.). Actas de la Conferencia Internacional sobre Teoría y Práctica del Desarrollo de Software (TAPSOFT) . Lecture Notes in Computer Science. Vol. 493. Springer. pp. 169–192 .  
  8. ↑ Cousot, Patrick; Halbwachs, Nicolas (enero de 1978). "Descubrimiento automático de restricciones lineales entre variables de un programa" (PDF) . Actas de la conferencia del 5.º Simposio ACM sobre Principios de Lenguajes de Programación (POPL) . págs. 84–97 . 
  9. ↑ Miné, Antoine (2001). "Un nuevo dominio abstracto numérico basado en matrices de cotas de diferencia". En Danvy, Olivier; Filinski, Andrzej (eds.). Programas como objetos de datos, Segundo simposio, (PADO) . Lecture Notes in Computer Science. Vol. 2053. Springer. pp. 155–172 . arXiv : cs/0703073 .  
  10. ^ Miné, Antoine (diciembre de 2004). Dominios abstractos numéricos débilmente relacionales (PDF) (tesis doctoral). Laboratoire d'Informatique de l'École Normale Supérieure.
  11. ↑ Antoine Miné (2006). "El dominio abstracto del octágono". Símbolo de orden superior. Comput . 19 (1): 31– 100. arXiv : cs/0703084 . doi : 10.1007/s10990-006-8609-1 .
  12. ↑ Clarisó, Robert; Cortadella, Jordi (2007). "El dominio abstracto del octaedro". Science of Computer Programming . 64 : 115–139 . doi : 10.1016/j.scico.2006.03.009 . hdl : 10609/109823 .
  13. ↑ Michael Karr (1976). "Relaciones afines entre variables de un programa". Acta Informatica . 6 (2): 133– 151. doi : 10.1007/BF00268497 . S2CID 376574 . 
  14. ↑ Miné, Antoine (junio de 2012). "Dominios abstractos para operaciones de enteros y punto flotante a nivel de bits en máquinas" . WING'12 - 4.º Taller Internacional sobre Generación de Invariantes . Manchester, Reino Unido: 16.
  15. ↑ Regehr, John; Duongsaa, Usit (junio de 2006). «Derivación de funciones de transferencia abstractas para el análisis de software embebido» . Actas de la conferencia ACM SIGPLAN/SIGBED de 2006 sobre lenguaje, compiladores y soporte de herramientas para sistemas embebidos . LCTES '06. Nueva York, NY, EE. UU.: Association for Computing Machinery. págs. 34–43 . doi : 10.1145/1134650.1134657 . ISBN  978-1-59593-362-1. S2CID 13221224 . 
  16. ↑ Reps, T.; Loginov, A.; Sagiv, M. (julio de 2002). "Minimización semántica de fórmulas proposicionales trivalentes". Actas del 17.º Simposio Anual IEEE sobre Lógica en Ciencias de la Computación . págs. 40–51 . doi : 10.1109/LICS.2002.1029816 . ISBN  0-7695-1483-9. S2CID 8451238 . 
  17. ↑ Yoon, Yongho; Lee, Woosuk; Yi, Kwangkeun (2023-06-06). "Síntesis de programas inductiva mediante interpretación abstracta iterativa hacia adelante y hacia atrás" . Actas de la ACM sobre lenguajes de programación . 7 (PLDI): 174:1657–174:1681. arXiv : 2304.10768 . doi : 10.1145/3591288 .
  • Una página web sobre interpretación abstracta mantenida por Patrick Cousot.
  • El artículo de Roberto Bagnara muestra cómo es posible implementar un analizador estático basado en interpretación abstracta para un lenguaje de programación similar a C.
  • Las actas de los simposios de análisis estático aparecen en la serie Springer LNCS.
  • Conferencia sobre Verificación, Comprobación de Modelos e Interpretación Abstracta (VMCAI), afiliada a la conferencia POPL , cuyas actas aparecen en la serie Springer LNCS.
Apuntes de clase
  • Resumen e interpretación . Patrick Cousot. MIT.
  • Apuntes de clase de David Schmidt sobre interpretación abstracta
  • Apuntes de clase de Møller y Schwarzbach sobre análisis estático de programas.
  • Apuntes de clase de Agostino Cortesi sobre Análisis y Verificación de Programas.
  • Diapositivas de Grégoire Sutre que repasan cada paso de la interpretación abstracta con muchos ejemplos, introduciendo también las conexiones de Galois.