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.
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
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.
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:
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
Siendo:
un dominio concreto.
Dα la abstracción de dicho dominio.
α la función de abstracción.
γ la función de concretización.
es el conjunto partes de .
es la función concreta que representa al programa
la función de significado abstracto de una función FP.
es una función dependiente de FP que asigna conjuntos de entradas del programa a conjuntos de salida.
un elemento del dominio abstracto.
un elemento del dominio.
resultado/s de la función Fα
resultado/s de la función F*P.
Considere a λ, , λr y como representaciones o etiquetas y no el conjunto o dato en sí. Léase la línea 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 () 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 .
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 .
3.1 Propiedades de la interpretación abstracta
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
3.3 Función de concretización
Sea Dα un dominio abstracto y partes de (o "conjunto potencia de") un dominio concreto, se dice que es la función de concretización.
Por ejemplo, sea el dominio abstracto . Se puede definir a γ de la siguiente manera:
Es preciso dar la definición de : .
3.4 Función de abstracción
Sea D un dominio y Dα el dominio abstracto, se define a
como la función de abstracción.
Ejemplo:
3.5 Significado abstracto
La función se denomina función de significado abstracto.
3.5.1 Significado abstracto segura
Se dice que es segura si:
Por ejemplo: Sea un programa con entrada y salida .
Entonces la función que representa a este programa concreto es .
Abstrayéndolo con la función de significado abstracto se obtiene donde es la operación abstracta de los signos definida en los ejemplos anteriores.
Si el programa tiene como entrada un número positivo ( abstrayéndolo resulta en ), entonces se obtiene: .
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 es un retículo completo, entonces para todo , existe un único mínimo límite superior .
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
una función monótona de concretización.
una función monótona de abstracción.
La estructura se denomina inserción de Galois si cumple con lo siguiente:
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 . Se dice que se aproxima de forma segura a sssi .
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 y dos funciones monótonas y .
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 se refleja dentro de la aplicación de .
En otras palabras aplicar refleja/mapea/aproxima a 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
4.1 Semántica de Punto Fijo
4.1.1 Definiciones
Un lenguaje de primer orden , asociado a un programa .
Sea el Universo de Herbrand: El conjunto de todos los términos básicos de
Sea la sa Base de Herbrand: El conjunto de todos los átomos instanciados (ground) de .
Una Interpretación de Herbrand es un subconjunto de .
Sea 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 el operador de consecuencia inmediata. Está definido por:
es el procedimiento para obtener el mínimo punto fijo comenzando desde .
Observar que la definición de TP depende del programa P.
Considerar 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:
El Universo de Herbrand es:
La Base de Herbrand es:
El conjunto de todas las interpretaciones de Herbrand es:
Un modelo de Herbrand es:
El procedimiento para obtener el mínimo punto fijo es:
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
Función de concretización: γ
Función de abstracción: α
Operador abstracto: TαP
Es la versión abstracta de TP
Inserción de Galois:
Considerar que TαP depende del programa abstracto Pα (sería correcto decir en vez de TαP).
Para demostrar exactitud o terminación se debe:
Exactitud:
Iα es un retículo completo
Iα Debe aproximar a
TαP es una aproximación segura de TP
i.e.
Terminacion:
TαP es monótono
Iα cadena ascendente finita.
Con esto se puede deducir que donde:
es el número de pasos (finito)
aproximará a .
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.
Figura 7: Relación entre los elementos relevantes de la interpretación abstracta Bottom-Up. fig:intabs_bottom_up
Sea el conjunto de símbolos de predicado en el programa P, se obtiene:
La función de abstracción se define como:
La función de concretización se define como:
Por consiguiente, la versión abstracta de es se obtiene de la siguiente manera:
Por consiguiente, los "tipos" de datos deducidos son . Obsérvese que Hα es la aproximación al modelo de Herbrand (todas las consecuencias lógicas del programa P).
Para utilizar el programa en Ciao Prolog se debe escribir lo siguiente:
En congruencia con los resultados de 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.