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

Presentación: HTML | Fuentes
Fuentes de este apunte: Repositorio en Github
Códigos usados: Ver directorio ./tangled/
Descargar códigos y fuentes completo: Descargar ZIP completo (O ir al repositorio de Github).

https://i.creativecommons.org/l/by-sa/4.0/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.

Aserciones

Formato

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

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

La tabla ref: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 ref: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.

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

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).

Aserciones: info:ciao#The Ciao assertion language.
Tipos de datos básicos y propiedades: info:ciao#Basic data types and properties (predicados como term/1, atm/1, list/1, list/2, num/1, etc.).
Aserciones de computabilidad: info:ciao#Properties which are native to analyzers.
Explicación de los tipos regulares: info:ciao#Declaring regular types.
Sintaxis para la documentation con PlDoc: info:ciao#Documentation comments.

Módulos a utilizar:

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

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.

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]).

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.

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.

Teoría

\begin{tikzpicture}
  [every annotation/.style={fill=red!20}]
  
  \path[mindmap,
    concept color=black,
    grow cyclic,
    text=white,
    level 1/.append style={sibling angle=90},
    %% level 2/.append style={sibling distance=1cm},
    every node/.style={concept}
  ]
  %
  node {Interpretación Abstracta}
  %
  child[concept color=violet]{node (semcol) {Semántica colectoras}
    child{node {Retículos ``Se aproxima mejor''}}
    child{node {Inserción de Galois}
      child{node {\scriptsize Aprox. segura}}
      child[concept color=red!50!black]
      {node {\scriptsize Teorema fundamental}}
    }
  }
  %
  child[concept color=blue!50!black]{node {Aproxi\-maciones}
    child {node {Aproxi\-mación correcta}
      child {node {Idea básica}}
      child {node {De una fnc.}}
    }
    child {node {De un programa}
      child{node{$F_P$ (concreto)}}
      child{node{$F_P^*$}}
    }
    child {node (sigabs) {Significado abstracto $F_\alpha$}
      child{node {Se\-gu\-ri\-dad}}
    }
  }
  %
  child[concept color=orange]{node (domabs) {Dominio abstracto}
    child{node {Función de concretización\\$\gamma$}}
    child{node {Función de abstracción\\$\alpha$}}
  }
  %
  child[concept color=green!50!black]{node {Propiedades}
    child{node{Exactitud}
      child[concept color=blue!50!black]{
        node{\scriptsize Aprox. correcta}}
    }
    child{node{Termi\-nación}}
    child{node{Eficiencia}}
    child{node{Precisión}}
    child{node{Utilidad}}
  };


  \node[annotation, below right] at (semcol.south east) (annsemcol) {\scriptsize No alcanza con definir ``entrada-salida''. Se necesita información de ``estado'' en cada punto del programa.};

  
  \tikzstyle{every node}=[draw]
  \node[above right=2.5cm of domabs] (domabsimg) {%%
    \includegraphics[width=8cm]{%%
      /home/poo/repos/curso-AILP/imgs/alphagamma.png}};  
  \node[right=2.5 of sigabs] (sigabsimg) {%%
    \includegraphics[width=7cm]{%%
      /home/poo/repos/curso-AILP/imgs/absmean.png}};

  \draw[arrows=->, ultra thick, orange]
  (domabs) edge (domabsimg.south west);
  \draw[arrows=->, ultra thick, blue!50!black, bend right]
  (sigabs) edge (sigabsimg);
  \draw[arrows=->, ultra thick, violet, bend left]
  (semcol) edge (annsemcol);
\end{tikzpicture}

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 → D$ es la función concreta que representa al programa $P$
$F_α D_α → D_α$ la función de significado abstracto de una función F_P.
$F_P^* : \wp(D) → \wp(D) \quad F_P^*(S) = \{F_P(x) | x ∈ S\}$ es una función dependiente de F_P que asigna conjuntos de entradas del programa a conjuntos de salida.
$λ ∈ D_α$ un elemento del dominio abstracto.
$d ∈ D$ un elemento del dominio.
$\lamda_r$ resultado/s de la función F_α
$d_r$ resultado/s de la función F^*_P.

Considere a λ, $d$, λ_r y $r$ como representaciones o etiquetas y no el conjunto o dato en sí. Léase la línea $d → λ$ 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$.

Propiedades de la interpretación abstracta

\begin{tikzpicture}
  \path[mindmap, concept color=black, text=white]
  %
  node[concept,align=center]{Propiedades de la\\Interpretación Abstracta}
  [clockwise from=35]
  child[concept color=red!50!black] {
    node[concept] {Requeridas}
    child {node[concept] (exac) {Exactitud}}
    child {node[concept] (term) {Terminación}}
  }
  %
  child[concept color=green!50!black]{
    node[concept] {Deseables}
    child {node[concept] (efic) {Eficiencia}}
    child {node[concept] (prec) {Precisión}}
    child {node[concept] (util) {Utilidad}}
  };

  \node[annotation, right=of exac, fill=red!20] {\small Aproximaciones correctas. La aproximación sea lo más conservadora posible.};
  \node[annotation, right=of term, fill=red!20] {\small La compilación debe terminar.};
  \node[annotation, right=of efic, fill=red!20] {\small Tiempo de análisis debe ser finito y lo más pequeño posible.};
  \node[annotation, right=of prec, fill=red!20] {\small Precisión en la información recopilada.};
  \node[annotation, right=of util, fill=red!20] {\small Determinar qué información vale la pena recopilar.};

\end{tikzpicture}

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.

Aproximaciones correctas

\begin{tikzpicture}
  \path[mindmap, concept color=black, text=white]
  %
  node[concept,align=center]{Aproximaciones Correctas}
  [clockwise from=35]
  child[concept color=green!50!black] {
    node[concept] {Para una propiedad $p$}
    child[grow=0] {node[concept]
      {dpq': $\forall x, x \in S \Rightarrow p(x)$}
      child {node[concept] {\scriptsize Alter\-na\-ti\-va}
        [grow'=right, sibling distance=1.75cm]
        %
        child{node[concept, align=center]
          {\scriptsize Cons\-tru\-ir}
          child[concept color=white!20]{node[concept, text=black]
            {\scriptsize un cjto. $S_a \supseteq S$}
          }
        }
        %
        child{node[concept]
          {\scriptsize Demos\-trar}
          child[concept color=white!20]{node[concept, text=black]
            {\scriptsize $\forall x x \in S_a \Rightarrow p(x)$}
          }
        }
        %
        child[concept color=red!50!black]{node[concept]
          {\scriptsize $\therefore$}
          child{node[concept]
            {\scriptsize $S_a$ es una aprox. segura de $S$}
          }
        }
      }
    }
  }
  %%
  child[concept color=green!50!black] {
    node[concept] {Para una función $F$}
    child[grow=0, level distance=3.5cm] {node[concept]
      {dpq': $\forall x$ $x \in S \Rightarrow p(F(x))$}
      [grow'=right, sibling distance=1.75cm]
      child[level distance=2.5cm] {node[concept]
        {\scriptsize Buscar}
        child[concept color=white!20]{node[concept, text=black]
          {\scriptsize una fnc. $G: S \rightarrow S$}
        }
      }
      child[level distance=2.5cm] {node[concept]
        {\scriptsize Demos\-trar}
        child[concept color=white!20]{node[concept, text=black]
          {\scriptsize $\forall x, x \in S p(G(x)) \Rightarrow p(F(x))$}
        }
      }
      child[level distance=2.5cm, concept color=red!50!black] {node[concept]
        {\scriptsize $\therefore$}
        child{node[concept]
          {\scriptsize $G$ es una aprox. segura de $S$}
        }
      }
    }
  };
\end{tikzpicture}

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 $γ : D_α → \wp(D)$ es la función de concretización.

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

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

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

Función de abstracción

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

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

Significado abstracto

La función $F_α : D_α → D_α$ se denomina función de significado abstracto.

Significado abstracto segura

Se dice que $F_α$ es segura si:

$$∀ λ, λ ∈ D_α, γ(F_α(λ)) \supseteq F^*_P(γ(λ))$$

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_α = x *_α [-]$ donde $*_α$ 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_α([+])$), entonces se obtiene: $F_α([+]) = [+] *_α [-] = [-]$.

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.

Estructura de Retículo

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

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

Inserción de Galois

Sea:

D y D_α retículos completos
$γ : D_α → D$ una función monótona de concretización.
$α : D → D_α$ una función monótona de abstracción.

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

$∀ λ ∈ D_α . λ = α(γ(λ))$
$∀ d ∈ D . d \subseteq γ(α(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 γ.

Aproximación Segura

Sea una inserción de Galois $(D_α, γ, D, α)$. Se dice que $λ ∈ D_α$ se aproxima de forma segura a $d ∈ D$ sssi $d \subseteq γ(λ)$.

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

Teorema fundamental

Dada una inserción de Galois $(D_α, γ, D, α)$ y dos funciones monótonas $F : D → D$ y $F_α : D_α → D_α$.

Si F_α es una aproximación de F entonces lfp(F_α)[fn:1] es una aproximación de lfp(F).

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

En otras palabras aplicar $lfp(F_α)$ 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.

Análisis de Programas Lógicos

\begin{tikzpicture}
  [every annotation/.style={fill=red!20}]
  
  \path[mindmap,
    concept color=black,
    grow cyclic,
    text=white,
    level 1/.append style={sibling angle=80},
    %% level 2/.append style={sibling distance=1cm},
    every node/.style={concept}
  ]
  %
  node {Análisis de Programas Lógicos}
  %
  child {node {Casos intermedios/misc}}
  % 
  child[concept color=blue!50!black] {node (semope) {Semántica operativa}
    child[concept color=red!20, text=black] {node {a.k.a. ``Top-Down''}}
    child {node {De\-no\-ta\-cio\-nal}}
    child {node {Basada en SLD}
      child {node {\scriptsize ...}}
      child {node {\scriptsize Reac\-ti\-vo}}
      child {node {\scriptsize Pa\-ra\-le\-lo}}
    }
  }
  %
  child[concept color=green!50!black] {node (semdec) {Semántica declarativa}
    child[concept color=red!20, text=black] {node {a.k.a. ``Bottom-Up''}}
    child {node {Semántica de modelos mínimos}}
    child {node {Semántica de punto fijo}
      child[concept color=red!20, text=black] {
        node {\scriptsize ba\-sa\-da en $T_P$}}
    }
  };

  \node[annotation, left] at (semdec.west)
  {\scriptsize Relacionada con las consecuencias lógicas del programa};
  \node[annotation, above left=0.4cm of semope.north east]
  {\scriptsize Cercana al comportamiento del programa};
\end{tikzpicture}

Semántica de Punto Fijo

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 → I$ el operador de consecuencia inmediata. Está definido por:

\begin{align*} T_P(M) =& \{h ∈ B | ∃ C ∈ ground(P)
& C = h ← b_1, \ldots, b_n \mbox{ y } \ & b_1, \ldots, b_n ∈ M\} \end{align*}

$T_P ↑ ω$ es el procedimiento para obtener el mínimo punto fijo comenzando desde $ω = 1$.

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

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

Ejemplo

Sea el siguiente programa P:

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

Escrito formalmente:

$P = \{ p(f(X)) ← 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 ↑ 0 &= \{ p(a),q(a),q(b) \}
T_P ↑ 1 &= \{ p(a),q(a),q(b),p(f(a)) \} \ T_P ↑ 2 &= \{ p(a),q(a),q(b),p(f(a)),p(f(f(a))) \} \ \ldots \ T_P ↑ ω &= H \end{align*}

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

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: γ
- $γ : I^α → I$
Función de abstracción: α
- $α : I → I^α$
Operador abstracto: T^α_P
- Es la versión abstracta de T_P
- $T^α_P : I^α → I^α$
Inserción de Galois: $(I^α, γ, I, α)$

Considerar que T^α_P depende del programa abstracto P_α (sería correcto decir $T^α_{P_{α}}$ 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: ∀ M ∈ I, γ(α(M)) \supseteq M$
- T^α_P es una aproximación segura de T_P
  - i.e. $∀ d, d ∈ I^α, γ(T^α_P(d)) \supseteq T_P(γ(d))$
Terminacion:
- T^α_P es monótono
- I^α cadena ascendente finita.

Con esto se puede deducir que $H^α = lfp(T^α_P) = T^α_P ↑ n$ donde:

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

La Figura ref: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.

Ejemplo de inferencia de “tipos”

Sea el siguiente programa lógico P:

\begin{align*} P = \{ & p(f(X)) ← p(X).
& p(a).\ & r(X) ← 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_α = \{ & p ← p.
& p.\ & r ← t.\ & q.\} \end{align*}

Sea $B^α = 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 $α : I → S^*$ se define como:

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

La función de concretización $γ : S^* → I$ se define como:

\begin{align*} γ(\{p/1, q/1\}) & = \{ A ∈ B \;|\; pred(A) = p/1 \; ∨ \; 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^α_P : S^* → S^*$ se obtiene de la siguiente manera:

\begin{align*} T^α_P ↑ 0 &= T^α_P(∅) = \{ p/1, q/1 \}
T^α_P ↑ 1 &= T^α_P(\{ p/1, q/1 \}) \ &= \{ p/1, q/1 \} \ &= T^α_P ↑ 0 = H^α \end{align*}

Por consiguiente, los “tipos” de datos deducidos son $\{ p/1, q/1 \} = H^α$. 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^α$ 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.

Footnotes

[fn:1] lfp significa least fixed point. gfp significa greatest fixed point.

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

index.org

index.org

Aserciones

Formato

Azúcares sintácticos

regtype

comp

Checking

Teoría

Propiedades de la interpretación abstracta

Aproximaciones correctas

Función de concretización

Función de abstracción

Significado abstracto

Significado abstracto segura

Semánticas colectoras

Estructura de Retículo

Inserción de Galois

Aproximación Segura

Teorema fundamental

Análisis de Programas Lógicos

Semántica de Punto Fijo

Definiciones

Ejemplo

Interpretación abstracta “Bottom Up”

Ejemplo de inferencia de “tipos”

Footnotes

Meta

Files

index.org

Latest commit

History

index.org

File metadata and controls

Aserciones

Formato

Azúcares sintácticos

regtype

comp

Checking

Teoría

Propiedades de la interpretación abstracta

Aproximaciones correctas

Función de concretización

Función de abstracción

Significado abstracto

Significado abstracto segura

Semánticas colectoras

Estructura de Retículo

Inserción de Galois

Aproximación Segura

Teorema fundamental

Análisis de Programas Lógicos

Semántica de Punto Fijo

Definiciones

Ejemplo

Interpretación abstracta “Bottom Up”

Ejemplo de inferencia de “tipos”

Footnotes

Meta