UP | HOME

Apuntes del Curso Análisis Estático de Programas Lógicos

El siguiente es una apunte del curso Análisis Estático de Programas Lógicos Basado en Interpretación Abstracta.

88x31.png

This work is licensed under a Creative Commons Attribution-ShareAlike 4.0 International License.

Este obra está bajo una licencia de Creative Commons Reconocimiento-CompartirIgual 4.0 Internacional.

Los mismos términos utilizados en Ciao Prolog (definiciones de term, atom, predicate, etc.) también se pueden encontrar en el glosario de SWI-Prolog.

1 Aserciones

1.1 Formato

Normalmente, el formato de las aserciones en prolog sigue al siguiente estructura: 

:- [estado] [aserción] [pred] [: precond] [=> postcond] [+ propcomp] [# "comentario"]

La tabla tab:aserciones_estados describe los distintos valores del campo [estado]. Éstos pueden ser escritos por el usuario o por CiaoPP como salida del chequeo. Los estados que mayormente se escriben por el usuario es trust y check.

Los tipos de aserciones que se escriben en el campo [aserción] están detallados en la tabla tab:aserciones_tipos.

Usualmente, una aserción es interpreta de la siguiente manera:

  • [pred] es la llamada al predicado (goal) y debe ser cierta.
  • [: precond] si existe debe ser verdadera.
  • Entonces, [=> postcond] debe complirse, en cuyo caso el preprocesador retornará true o checked en el [estado].
  • La propiedad de computaciónd indicada en [+ propcomp] debe cumplirse.

Si [pred] o [: precond] no se cumple, no se chequea la postcondición ni al propiedad de computabilidad. La aserción queda en forma de warning con check como estado.

Tabla 1 Estados posibles de la aserción. tab:aserciones_estados
Estado Significado
trust Ingresada por el usuario,
  confiar en la veracidad de la aserción.
checked La aserción fue verificada
true Salida del compilador.
false Error de compilación
check Aserción con warnings, chequear aserción.
  • AS: Azúcar Sintáctico
Tabla 2 Tipos de aserciones y su significado. tab:aserciones_tipos
Aserción Significado AS
pred Equivalente a calls, success y comp juntos sí
  (dependiendo de los campos completados).  
calls La llamada del predicado debe satisfacer  
  la precondición indicada.  
entry Similar a calls pero declara la llamadas  
  exportadas. Son confiadas por el compilador.  
comp Toda llamada del predicado que cumpla con la  
  precondición, debe cumplir con la propiedad  
  de la computación dada.  
regtype Declara un tipo regular.  
success El predicado que cumpla con la precondición  
  y retorne éxito debe verificar la postcondición.  
doc Documentación utilizada por Pldoc  
test Testeo con instancias. Similar a success.  

test no se verifica con CiaoPP porque no trabaja con dominios abstractos.

Más información en los manuales de info (en Emacs posicionar el cursor sobre un link y presionar C-c C-o).

Módulos a utilizar:

  • assertions
  • regtypes
  • nativeprops
  • basic_props (este módulo es importado automáticamente con assertions)

1.1.1 Azúcares sintácticos

pred qsort(A,B) : (list(A), var(B)) => list(B) + not_fails.

Es equivalente a lo siguiente: 

:- calls qsort(A,B) : (list(A), var(B)).
:- success qsort(A,B) : (list(A), var(B)) => list(B).
:- comp qsort(A,B) : (list(A) , var(B)) + not_fails.

1.2 regtype

Para utilizar regtype, se debe agregar el módulo regtypes. Más información en: info:ciao#Declaring regular types.

Declara como tipos regulares un predicado. En otras palabras, declararía un dominio abstracto. Luego se puede utilizar en otras aserciones para chequear que una varible está en un dominio.

Por ejemplo, en el código del autómata se puede utilizar el tipo regtype para declarar el tipo car/1 y en el entry se declara que C es una lista con dominio en car/1 y S de tipo initial/1 

:- module(aut, _, [assertions, regtypes]).

:- entry accepts_(S,C) : (initial(S), list(car, C)).
:- regtype car/1.

car(a).
car(b).

%% ...
accepts_(State, []) :-
    final(State).
%% ...

El analizador de código de CiaoPP puede generar nuevos regtypes para declarar nuevos dominios. Por ejemplo, en el siguiente código se generan dos regtypes, rt4/1 y rt5/1 definiendo los dominios de las dos variables de te/2. 

:- module(app, _, [assertions, nativeprops]).

te(1, "hello").
te(0, 0).

La salida del analizador es la siguiente: 

:- module(_1,_2,[assertions,nativeprops,regtypes]).

:- true pred te(_A,_B)
   : ( term(_A), term(_B) )
   => ( rt4(_A), rt5(_B) ).

:- true pred te(_A,_B)
   : mshare([[_A],[_A,_B],[_B]])
   => ground([_A,_B]).

te(1,"hello").
te(0,0).


:- regtype rt4/1.
rt4(0).
rt4(1).

:- regtype rt5/1.
rt5(0).
rt5([104,101,108,108,111]).

1.3 comp

Varios de los predicados para comp están definidos en el módulo assertions/native_pros. Es necesario incluirlo en el preámbulo module como nativeprops. Por ejemplo: 

:- module(the_file, _, [assertions, nativeprops]).

O sino, se puede agregar como módulo: 

:- use_module(library(assertions/native_props)).

Más información en: info:ciao#Properties which are native to analyzers

Algunos predicados para chequeo de computación interesantes son: not_fails, no_choicepoints, possibly_fails, fails, non_det, is_det, possibly_nondet, finite_solutions, terminates, exception, no_exception, possible_exceptions.

2 Checking

CiaoPP trabaja sobre dominios abstractos y no concretos. Por ello, test no funcionaría si se brindan datos concretos. En ese caso utilizar los testeos de unidad.

Los dominios abstractos se irán creando a medida que sea necesario con nombres de la forma rtNNN donde NNN es un número. A menos que se declaren con regtype/1.

Se puede utilizar el predicado output/0 en la consola CiaoPP para obtener el archivo con los resultados del análisis y el chequeo.

3 Teoría

summary.png

Siendo:

  • $D$ un dominio concreto.
  • Dα la abstracción de dicho dominio.
  • α la función de abstracción.
  • γ la función de concretización.
  • $\wp (D)$ es el conjunto partes de $D$.
  • $F_{P} : D \to D$ es la función concreta que representa al programa $P$
  • $F_\alpha D_\alpha \to D_\alpha$ la función de significado abstracto de una función FP.
  • $F_{P}^{*} : \wp(D) \to \wp(D) \quad F_P^*(S) = \{F_P(x) | x \in S\}$ es una función dependiente de FP que asigna conjuntos de entradas del programa a conjuntos de salida.
  • $\lambda \in D_\alpha$ un elemento del dominio abstracto.
  • $d \in D$ un elemento del dominio.
  • $\lamda_r$ resultado/s de la función Fα
  • $d_r$ resultado/s de la función F*P.

absmean.png

Considere a λ, $d$, λr y $r$ como representaciones o etiquetas y no el conjunto o dato en sí. Léase la línea $d \to \lambda$ usando α de la siguiente manera: "para representar los valores que existen en lo concreto (d) a lo abstracto (λ) se utiliza la función de abstracción (α)".

En la zona superior se representa un gráfico similar al de la figura que apunta "Dominio abstracto" en el mapa mental. Se resume en que dado un programa y su datos concretos ($d$) se puede obtener su abstracción con α. Y se puede volver a obtener estos datos concretos utilizando la función γ.

En la zona inferior se representa los resultados de aplicar la función que representa al programa sea en abstracto o concreto.

Del lado derecho, se muestra el programa concreto y al aplicarse la función F*P sobre un conjunto de entradas se obtiene las salidas $r$.

Del lado izquierdo, se presenta la abstracción λ de las entradas, que al aplicarse la función de abstracción Fα resulta en λ_r. Este resultado, al concretizarse con γ se obtiene un superconjunto de los resultados dados en $r$.

3.1 Propiedades de la interpretación abstracta

1.props_interp_abstr.png

Propiedades:

  • Exactitud: La aproximación realizada (el análisis realizado) ¿es lo más exacto posible? ¿se equivoca dentro de lo esperado? ¿no brinda resultados inconsistentes?
  • Terminación: ¿La compilación termina con un resultado?
  • Eficiencia: El tiempo de análisis, ¿es el menor? ¿es finito?
  • Precision: La información obtenida ¿es precisa?¿brinda un buen detalle de información del/de los programa/s?
  • Utilidad: La abstracción, ¿tiene alguna utilidad?. La información que ofrece, ¿vale la pena?
  • Precisión: Ejemplo: el análisis puede indicarnos que el resultado de un programa es un tipo de dato numérico. Pero sería más preciso si nos indica que es un número positivo. Más aún si indica que es un número positivo y par.

3.2 Aproximaciones correctas

2.aprox_correctas.png

3.3 Función de concretización

Sea Dα un dominio abstracto y $\wp(D)$ partes de (o "conjunto potencia de") un dominio concreto, se dice que $\gamma : D_\alpha \to \wp(D)$ es la función de concretización.

Por ejemplo, sea el dominio abstracto $D_\alpha = \{ [-],[0],[+], \top \}$. Se puede definir a γ de la siguiente manera:

\begin{align*} \gamma([-]) &= \{x \in Z \arrowvert x < 0 \} \\ \gamma([0]) &= \{0\} \\ \gamma([+]) &= \{x \in Z \arrowvert x > 0\} \\ \gamma(\top) &= Z \end{align*}

Es preciso dar la definición de $\bot$ : $\gamma(\bot) = \emptyset$.

3.4 Función de abstracción

Sea D un dominio y Dα el dominio abstracto, se define a $\alpha : \wp(D) \rightarrow D_\alpha$ como la función de abstracción.

Ejemplo: $\alpha({1,2,3}) = [+]$

3.5 Significado abstracto

La función $F_\alpha : D_\alpha \to D_\alpha$ se denomina función de significado abstracto.

3.5.1 Significado abstracto segura

Se dice que $F_\alpha$ es segura si:

$$\forall \lambda, \lambda \in D_\alpha, \gamma(F_\alpha(\lambda)) \supseteq F^*_P(\gamma(\lambda))$$

Por ejemplo: Sea $P = (y := x * -3)$ un programa con entrada $x$ y salida $y$. Entonces la función que representa a este programa concreto es $F_P = x * -3$. Abstrayéndolo con la función de significado abstracto se obtiene $F_\alpha = x *_\alpha [-]$ donde $*_\alpha$ es la operación abstracta de los signos definida en los ejemplos anteriores.

Si el programa tiene como entrada un número positivo ($F_P(x) : x > 0$ abstrayéndolo resulta en $F_\alpha([+])$), entonces se obtiene: $F_\alpha([+]) = [+] *_\alpha [-] = [-]$.

3.6 Semánticas colectoras

La semántica I/O que se viene tratando es muy escueta. El análisis de semánticas extendidas se basa en deducir información sobre el estado en los puntos de programa (fixedpoints). Pero diferentes puntos de programa pueden alcanzarse bajo diferentes estados y desde diferentes puntos. Por ello, se necesita calcular una colección semántica de estados abstractos para un punto de programa.

Se puede aumentar la eficiencia si se "resume" la semántica recolectada (collecting semantics). Para ello se puede utilizar la estructura de retículo (lattice) en el dominio abstracto.

3.6.1 Estructura de Retículo

Se puede estrablecer una operación de orden ≤α sobre el dominio abstracto Dα. Si $(D_\alpha, \le_\alpha)$ es un retículo completo, entonces para todo $S \subseteq D_\alpha$, existe un único mínimo límite superior $\sqcup S \in D_\alpha$.

El retículo se usa para "resumir" la semántica recolectada de los resultados que se van obteniendo en cada fixpoint.

3.7 Inserción de Galois

Sea:

  • D y Dα retículos completos
  • $\gamma : D_\alpha \to D$ una función monótona de concretización.
  • $\alpha : D \to D_\alpha$ una función monótona de abstracción.

La estructura $(D_\alpha, \gamma, D, \alpha)$ se denomina inserción de Galois si cumple con lo siguiente:

  • $\forall \lambda \in D_\alpha . \lambda = \alpha(\gamma(\lambda))$
  • $\forall d \in D . d \subseteq \gamma(\alpha(d))$

La primer propiedad significa que si se aplica la concretización sobre un resultado abstracto (ej. números positivos $[+]$), y luego la volvemos a abstraer debe dar el mismo resultado y se mantiene consistente.

La segunda propiedad significa que si se intenta aplicar la abstracción sobre un resultado particular y luego la concretización, el resultado del cual partimos debe estra en el resultado final de γ.

3.7.1 Aproximación Segura

Sea una inserción de Galois $(D_\alpha, \gamma, D, \alpha)$. Se dice que $\lambda \in D_\alpha$ se aproxima de forma segura a $d \in D$ sssi $d \subseteq \gamma(\lambda)$.

Una aproximación es segura si al aplicar la función de concretización sobre un elemento abstracto si d.

3.7.2 Teorema fundamental

Dada una inserción de Galois $(D_\alpha, \gamma, D, \alpha)$ y dos funciones monótonas $F : D \to D$ y $F_\alpha : D_\alpha \to D_\alpha$.

Si Fα es una aproximación de F entonces lfp(Fα)1 es una aproximación de lfp(F).

El teorema fundamental justifica que la aplicación del $lfp(F_\alpha)$ se refleja dentro de la aplicación de $lfp(F)$.

En otras palabras aplicar $lfp(F_\alpha)$ refleja/mapea/aproxima a $lfp$ aplicado a la función que representa nuestro programa concreto, ofreciendo seguridad de que la abstracción aún representa nuestro programa.

4 Análisis de Programas Lógicos

analisis_programas_logicos.png

4.1 Semántica de Punto Fijo

4.1.1 Definiciones

  • Un lenguaje de primer orden $L$, asociado a un programa $P$.
  • Sea $U$ el Universo de Herbrand: El conjunto de todos los términos básicos de $L$
  • Sea $B$ la sa Base de Herbrand: El conjunto de todos los átomos instanciados (ground) de $L$.
  • Una Interpretación de Herbrand es un subconjunto de $B$.
  • Sea $I$ es el conjunto de todas las interpretaciones de Herbrand.
  • Un Modelo de Herbrand es una interpretación de Herbrand que contiene todas las consecuencias del programa.
  • Sea $T_P : I \to I$ el operador de consecuencia inmediata. Está definido por:

\begin{align*} T_P(M) =& \{h \in B \vert \exists C \in ground(P) \\ & C = h \leftarrow b_1, \ldots, b_n \mbox{ y } \\ & b_1, \ldots, b_n \in M\} \end{align*}

  • $T_P \uparrow \omega$ es el procedimiento para obtener el mínimo punto fijo comenzando desde $\omega = 1$.

Observar que la definición de TP depende del programa P.

Considerar $ground(P)$ como el conjunto de todos los términos instanciados de P.

4.1.2 Ejemplo

Sea el siguiente programa P: 

p(f(X)) :- p(X).
p(a).
q(a).
q(b).

Escrito formalmente:

$P = \{ p(f(X)) \leftarrow p(X). p(a). q(a). q(b). \}$

El Universo de Herbrand es:

$$U = \{ a,b,f(a),f(b),f(f(a)),f(f(b)),\ldots \}$$

La Base de Herbrand es:

$$B = \{ p(a),p(b),q(a),q(b),p(f(a)),p(f(b)),p(f(f(a))), p(f(f(b))), q(f(a))\ldots \}$$

El conjunto de todas las interpretaciones de Herbrand es:

$$I = \mbox{ todos los subconjuntos de } B$$

Un modelo de Herbrand es:

$$H = \{ q(a), q(b), p(a), p(f(a)), p(f(f(a))), \ldots \}$$

El procedimiento para obtener el mínimo punto fijo es:

\begin{align*} T_P \uparrow 0 &= \{ p(a),q(a),q(b) \}\\ T_P \uparrow 1 &= \{ p(a),q(a),q(b),p(f(a)) \} \\ T_P \uparrow 2 &= \{ p(a),q(a),q(b),p(f(a)),p(f(f(a))) \} \\ \ldots \\ T_P \uparrow \omega &= H \end{align*}

Como consecuencia TP ↑ ω obtiene todas las consecuencias lógicas del programa.

4.1.3 Interpretación abstracta "Bottom Up"

Aplicar la interpretación abstracta consiste en definir lo siguiente:

  • Un dominio abstracto: Iα
    • donde sus elementos son aproximaciones de elementos de $I = \wp(B)$
  • Función de concretización: γ
    • $\gamma : I^\alpha \to I$
  • Función de abstracción: α
    • $\alpha : I \to I^\alpha$
  • Operador abstracto: TαP
    • Es la versión abstracta de TP
    • $T^\alpha_P : I^\alpha \to I^\alpha$
  • Inserción de Galois: $(I^\alpha, \gamma, I, \alpha)$

Considerar que TαP depende del programa abstracto Pα (sería correcto decir $T^{\alpha}_{P_{\alpha}}$ en vez de TαP).

Para demostrar exactitud o terminación se debe:

  • Exactitud:
    • Iα es un retículo completo
    • Iα Debe aproximar a $I: \forall M \in I, \gamma(\alpha(M)) \supseteq M$
    • TαP es una aproximación segura de TP
      • i.e. $\forall d, d \in I^\alpha, \gamma(T^\alpha_P(d)) \supseteq T_P(\gamma(d))$
  • Terminacion:
    • TαP es monótono
    • Iα cadena ascendente finita.

Con esto se puede deducir que $H^\alpha = lfp(T^\alpha_P) = T^\alpha_P \uparrow n$ donde:

  • $n$ es el número de pasos (finito)
  • $H^\alpha$ aproximará a $H$.

La Figura intabs_bottom_up muestra los elementos indicados anteriormente y la relación entre ellos. Obsérvese la separación entre los dos "dominios" de interpretación e interpretación abstracta y el uso de las funciones de concretización y abstracción para poder "ir y venir" entre ellos.

bottomup.png

Figura 7: Relación entre los elementos relevantes de la interpretación abstracta Bottom-Up. fig:intabs_bottom_up

4.1.4 Ejemplo de inferencia de "tipos"

Sea el siguiente programa lógico P:

\begin{align*} P = \{ & p(f(X)) \leftarrow p(X).\\ & p(a).\\ & r(X) \leftarrow t(X,Y).\\ & q(a).\\ & q(b). \} \end{align*}

En prolog: 

p(f(X)) :- p(X). 
p(a). 
r(X) :- t(X,Y). 
q(a). 
q(b).

La representación abstracta de P:

\begin{align*} P_\alpha = \{ & p \leftarrow p.\\ & p.\\ & r \leftarrow t.\\ & q.\} \end{align*}

Sea $B^\alpha = S$ el conjunto de símbolos de predicado en el programa P, se obtiene:

$$S = \{ p/1, q/1, r/1, t/2 \}$$

La función de abstracción $\alpha : I \to S^*$ se define como:

$$\alpha(\{p(a), p(b), q(a)\}) = \{ p/1, q/1 \}$$

La función de concretización $\gamma : S^* \to I$ se define como:

\begin{align*} \gamma(\{p/1, q/1\}) & = \{ A \in B \;|\; pred(A) = p/1 \; \vee \; pred(A) = q/1\} \\ & = \{p(a), p(b), p(f(a)), p(f(b)),\ldots, q(a), q(b), q(f(a)),\ldots \} \end{align*}

Por consiguiente, la versión abstracta de $T_P$ es $T^\alpha_P : S^* \to S^*$ se obtiene de la siguiente manera:

\begin{align*} T^\alpha_P \uparrow 0 &= T^\alpha_P(\emptyset) = \{ p/1, q/1 \} \\ T^\alpha_P \uparrow 1 &= T^\alpha_P(\{ p/1, q/1 \}) \\ &= \{ p/1, q/1 \} \\ &= T^\alpha_P \uparrow 0 = H^\alpha \end{align*}

Por consiguiente, los "tipos" de datos deducidos son $\{ p/1, q/1 \} = H^\alpha$. Obsérvese que Hα es la aproximación al modelo de Herbrand $H$ (todas las consecuencias lógicas del programa P).

Para utilizar el programa en Ciao Prolog se debe escribir lo siguiente: 

:- module(_, _, [assertions, nativeprops]).

p(f(X)) :- p(X). 
p(a). 
r(X) :- t(X,Y). 
q(a). 
q(b).

t(_,_).

El analizador de CiaoPP responde con la siguiente salida: 

:- module(_1,_2,[assertions,nativeprops,regtypes]).

:- true pred p(_A)
   : term(_A)
   => rt3(_A).

:- true pred p(_A)
   : mshare([[_A]])
   => ground([_A]).

p(f(X)) :-
    p(X).
p(a).

:- true pred r(X)
   : term(X)
   => term(X).

:- true pred r(X)
   : mshare([[X]])
   => mshare([[X]]).

r(X) :-
    t(X,Y).

:- true pred q(_A)
   : term(_A)
   => rt8(_A).

:- true pred q(_A)
   : mshare([[_A]])
   => ground([_A]).

q(a).
q(b).

:- true pred t(_1,_2)
   : ( term(_1), term(_2) )
   => ( term(_1), term(_2) ).

:- true pred t(_1,_2)
   : mshare([[_1],[_1,_2],[_2]])
   => mshare([[_1],[_1,_2],[_2]]).

t(_1,_2).


:- regtype rt3/1.
rt3(a).
rt3(f(A)) :-
    rt3(A).

:- regtype rt8/1.
rt8(a).
rt8(b).

En congruencia con los resultados de $H^\alpha$ planteados anteriormente, el analizador generó dos declaraciones de regtype denominadas rt3/1 y rt8/1. Al observarse los valores, se puede deducir que rt3/1 corresponde con los de p/1 y rt8/1 con los de q/1.

Nota al pie de página:

1

lfp significa least fixed point. gfp significa greatest fixed point.