Generación de casos de prueba tipo caja negra mediante restricciones

Universidad Complutense de Madrid Facultad de Inform´atica Departamento de Sistemas Inform´aticos y Computaci´on GENERACI ´ ON DE CASOS DE PRUEBA TIPO CAJA NEGRA MEDIANTE RESTRICCIONES Trabajo de Fin de Grado Doble Grado en Ingenier´ıa Inform´atica y Matem´aticas Junio 2018 Autor: Miguel Garrido Canalejas Director: Ricardo Pe˜na Mar´ı ii Miguel Garrido Canalejas Resumen La plataforma de validaci´on CAVI-ART nos ofrece una representaci´on intermedia de cualquier funci´on escrita en diferentes lenguajes de programaci´on, que incluye su c´odigo, su precondici´on y su postcondici´on. Sobre dicha funci´on deseamos realizar pruebas de ejecuci´on. El objetivo de este trabajo reside en crear de manera autom´atica diferentes casos de prueba que cumplan las precondiciones de las funciones que se quieran probar. Para ello, se han estudiado primero los resolutores SMT, en concreto Z3, se han programado en tal resolutor todas las funciones y tipos que pueden interesarnos para las precondiciones, y por ´ultimo se ha creado, en Haskell, un generador de restricciones que analice las precondiciones de un programa en la IR, gracias a su representaci´on en forma de ´arbol abstracto, y genere un archivo de restricciones procesable por Z3 con el que obtener los casos de prueba. Palabras clave Pruebas de ejecuci´on, resolutores SMT, generador de restricciones, resoluci´on de restricciones, estructuras de datos. iii iv Miguel Garrido Canalejas Abstract The validation platform CAVI-ART offers us an intermediate representation for any function written in different languages, including its precondition, its code and its postcondition. We want to do testing of those functions. The goal of this work consists of automatically creating different test cases satisfying the preconditions of the functions wanted to be tested. In order to do this, SMT solvers have been studied, specifically Z3, every function and datatype we could be interested in for the preconditions have been programmed, and, finally, a constraints generator has been created in Haskell. It analyzes the preconditions of an IR program, thanks to its abstract syntax tree representation, and generates a constraints file processable by Z3 from which we obtain the test cases. Keywords Testing, SMT solvers, constraints generator, constraints solving, data structures. v vi Miguel Garrido Canalejas ´ Indice general 1. Introducci´on 1 2. Preliminares 7 2.1. ProyectoCAVI-ART ........................... 7 2.2. Sistema actual de generaci´on de casos de prueba . . . . . . . . . . . . 7 2.3. LaherramientaZ3 ............................ 9 3. El lenguaje de asertos 15 3.1. Sintaxisb´asica .............................. 15 3.2. TipoLista................................. 16 3.3. TipoArray ................................ 19 3.4. Tipo ´ ArbolBinario............................ 23 3.5. Tipo ´ ArbolAVL ............................. 29 3.6. Tipo ´ ArbolRojinegro........................... 34 3.7. Doble uso de los predicados . . . . . . . . . . . . . . . . . . . . . . . 40 4. Estrategia de generaci´on de casos 45 4.1. Tipos de restricciones . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 4.1.1. Restricciones de tama˜no . . . . . . . . . . . . . . . . . . . . . 46 4.1.2. Restricciones de estructura . . . . . . . . . . . . . . . . . . . . 46 4.1.3. Restricciones de contenido . . . . . . . . . . . . . . . . . . . . 47 4.2. Estrategia ................................. 49 5. Experimentos 55 5.1. Listas ................................... 55 5.2. Arrays................................... 57 5.3. ´ ArbolesBinarios ............................. 59 vii viii ´ INDICE GENERAL 5.3.1. Mont´ıculos Zurdos . . . . . . . . . . . . . . . . . . . . . . . . 59 5.3.2. ´ Arboles de B´usqueda . . . . . . . . . . . . . . . . . . . . . . . 62 5.4. ´ ArbolesAVL ............................... 64 5.5. ´ ArbolesRojinegros ............................ 69 6. Conclusiones 77 A. Programa Haskell 81 A.1.Main.................................... 81 A.2.Ast2Smt.................................. 84 B. Resultados de Ejecuci´on 95 B.1.FicheroSmt................................ 95 B.2.FicheroTxt ................................ 97 Bibliograf´ıa 103 Miguel Garrido Canalejas Cap´ıtulo 1 Introducci´on Castellano Terminada la creaci´on de un cierto programa, aparece la tarea de hacer pruebas de ejecuci´on. Esta tarea consiste en comprobar si el programa se comporta como deber´ıa, mediante la ejecuci´on de una serie de casos de prueba, y la comparaci´on de los resultados obtenidos para dichos casos con las respectivas respuestas esperadas. Normalmente, especificar y preparar manualmente estos casos de prueba resulta tanto costoso como poco fiable. Es costoso porque requiere idear casos que se ajusten a nuestro c´odigo, realizar numerosas ejecuciones, determinar cu´al debe ser la respuesta correcta en cada caso y comprobar cada uno de los resultados. Por otro lado, la poca fiabilidad viene derivada de no considerar todos los casos necesarios, pues, ¿y si los casos elegidos son pocos o demasiado sencillos y dejan caminos sin explorar? Lo que creemos que est´a funcionando correctamente resulta tener errores que no hemos detectado. Automatizar todo este proceso parece entonces de sumo inter´es. Podemos clasificar las estrategias de pruebas en dos grandes grupos: de caja negra y de caja blanca [1]. La primera de ellas consiste en la generaci´on de casos de prueba bas´andose exclusivamente en la especificaci´on del programa, es decir, en las precondiciones y postcondiciones, sin importar el c´odigo de la funci´on. De este modo, los casos de prueba deber´an verificar la precondici´on, y el resultado obtenido tras la ejecuci´on deber´a satisfacer la postcondici´on. Por su parte, las pruebas de caja blanca tienen en cuenta el c´odigo del programa y su objetivo es generar casos que ejecuten los diferentes caminos que puede seguir la ejecuci´on dentro del c´odigo. Enmarcado dentro del proyecto CAVI-ART, explicado m´as adelante, este trabajo pretende automatizar las pruebas de caja negra mediante la generaci´on de casos de prueba que cumplan las precondiciones requeridas por las distintas funciones del programa. Dicho proyecto est´a enfocado fundamentalmente a la verificaci´on de programas, y por tanto cada funci´on est´a provista de precondici´on y postcondici´on. En trabajos previos sobre esta plataforma [2], se ha desarrollado una herramienta que transforma un aserto cualquiera en una funci´on ejecutable, de tal forma que se 1 8 CAP´ ITULO 2. PRELIMINARES Figura 2.1: Plataforma CAVI-ART posibles casos de prueba. Tras esto, se filtraban seg´un la precondici´on, descartando as´ı todos aquellos que no la cumplieran y que, por tanto, no eran v´alidos para verificar el programa. Este m´etodo resulta costoso tanto en tiempo como en recursos de memoria, puesto que estamos generando muchos casos para luego acabar descartando un alto porcentaje de ellos. El programa actual de generaci´on de casos de caja negra recibe como entrada un programa Haskell que se ajusta a la estructura de la Figura 2.3, con dos funciones booleanas referentes a la precondici´on y postcondici´on de la funci´on principal. De este modo, los casos de prueba deben ser valores para los argumentos de la funci´on x1:t1, . . . , xn:tn, donde tirefiere al tipo de la variable xi, puesto que son la entrada de la funci´on principal. Obviamente, la precondici´on especificar´a una serie de restricciones sobre estas variables de entrada. Por ello, los casos de prueba generados son los utilizados en la precondici´on para ver si se verifica o no. En caso de hacerlo, puede considerarse como un caso de prueba v´alido y, en caso contrario, es descartado. Los casos v´alidos se pasan por la funci´on, obteniendo as´ı un resultado final de la misma. Este resultado final, unido a los valores de las variables de entrada, son usados en la postcondici´on como argumentos para ver si cumplen todos los requisitos de salida necesarios. La tarea m´as complicada de este sistema reside en la generaci´on de valores para las variables de entrada de la precondici´on. Y es que, tales variables pueden ser Miguel Garrido Canalejas 2.3. LA HERRAMIENTA Z3 9 a::= c{constante } |x{variable } be ::= a{expresi´on at´omica } |f ai{aplicaci´on de funci´on/operador primitivo } | haii { construcci´on de tuplas } |C ai{aplicaci´on de constructor } e::= be {expresi´on ligada } |let hxi:: τii=be in e{let secuencial } |letfun defiin e{let recursivo para definici´on de funciones } |case aof alti[; →e]{case con rama default opcional } tldef ::= define {ψ1}def {ψ2} { definici´on de funci´on con precondici´on y postcondici´on } def ::= f(xi:: τi) :: yi:: τi=e{definici´on de funci´on (las variables de salida tienen nombre) } alt ::= C xi:: τi→e{rama del case } τ::= α{variable de tipo } |T τi{aplicaci´on de un constructor de tipo } Figura 2.2: Sintaxis abstracta de la IR preCD(x1:t1, . . . , xn:tn) : Bool fun(x1:t1, . . . , xn:tn) : t postCD(x1:t1, . . . , xn:tn, x :t) : Bool Figura 2.3: Estructura del programa Haskell recibido para las pruebas de caja negra de tipos simples como enteros o booleanos, pero tambi´en pueden ser de tipos tan complejos como listas, ´arboles rojinegros, o aquellos que el usuario desee inventarse. Para conseguir generar casos de prueba de forma correcta, es necesario entonces investigar el tipo de cada una de estas variables, para as´ı saber como asignarles posibles valores. Para ello, se utiliza la herramienta Template Haskell. Tal herramienta proporciona la posibilidad de analizar los tipos de cada m´etodo, accediendo a su definici´on para aquellos que son desconocidos (tipos algebraicos definidos en el programa). De este modo, una vez se tienen identificados cada uno de los tipos, el programa de caja negra genera todos los valores posibles hasta un cierto tama˜no fijado por el usuario para cada uno de ellos, logrando as´ı todas las asignaciones posibles para las variables que ir´an pas´andose por la precondici´on, funci´on principal y postcondici´on. 2.3. La herramienta Z3 El problema de la satisfactibilidad m´odulo teor´ıas (SMT del t´ermino Satisfiability Modulo Theories en ingl´es), es un problema de decisi´on para f´ormulas l´ogicas de primer orden, con respecto a ciertas teor´ıas subyacentes, como pueden Trabajo Fin de Grado 10 CAP´ ITULO 2. PRELIMINARES ser: la teor´ıa de los n´umeros enteros, la teor´ıa de los reales, la teor´ıa de los arrays o la de los bit-vectors. De este modo, dada una cierta f´ormula F, y bajo alguna de las teor´ıas previas, que nos restringen la interpretaci´on de los distintos s´ımbolos que aparecen en nuestra f´ormula, el problema consiste en determinar si Fes satisfactible. En este contexto aparecen lo que se denominan resolutores SMT. Se trata de herramientas encargadas de decidir la satisfactibilidad de una f´ormula concreta en su correspondiente teor´ıa. De entre los muchos que pueden encontrarse, uno de los m´as completos, y el que m´as se ajusta a nuestras necesidades, es Z3. Se trata de un resolutor SMT creado por Microsoft Research para la prueba de teoremas y la comprobaci´on de la satisfactibilidad de f´ormulas l´ogicas sobre una serie de teor´ıas. Modos de uso Un resolutor SMT, como es Z3, presenta dos modos de uso: determinar la satisfactibilidad de una serie de restricciones y obtener un modelo que las verifique, o establecer la validez de una f´ormula l´ogica. En el primer caso, Z3 trabaja con una serie de declaraciones de variables y funciones sobre las cuales se establecen una serie de restricciones para que cumplan ciertos requisitos. Una vez definidas todas estas restricciones mediante asertos, se pide a Z3 que compruebe si se pueden satisfacer, es decir, que busque si existe alguna combinaci´on de valores para las variables de modo que los asertos sean ciertos. En caso de que s´ı que lo sea, se le puede pedir adem´as que nos devuelva un modelo, es decir, una asignaci´on de valores a cada variable que hace que todas las restricciones se verifiquen. A la hora de pedir el modelo nos encontramos una limitaci´on, y es que ´unicamente nos devuelve una posible combinaci´on, cuando uno podr´ıa estar interesado en obtener m´as de una. En el segundo modo de uso, lo que se busca es determinar si una cierta f´ormula l´ogica es v´alida, es decir, si es siempre cierta para cualquier combinaci´on de valores. Si pidi´eramos a Z3 que comprobara la satisfactibilidad de tal f´ormula como hac´ıamos en el primer modo de uso, en caso de obtener que es satisfactible quiere decir que hay al menos una combinaci´on que hace cierta la f´ormula. Pero esto no nos es suficiente puesto que nosotros necesitamos que sea cierto para cualquier asignaci´on de valores y no para una particular. De este modo, el procedimiento consiste en negar nuestra f´ormula y pedir, ahora s´ı, que compruebe si se puede satisfacer. As´ı, si Z3 nos devuelve que esta f´ormula negada es insatisfactible, entonces podremos asegurar que la original era v´alida puesto que se hac´ıa cierta para valores cualesquiera. Entre los dos modos de uso explicados, nosotros utilizaremos el primero de ellos. Como ya hemos comentado previamente, buscamos generar una serie de casos de prueba para distintas funciones y que pueden tener que cumplir una serie de condiciones que constituyen la precondici´on. Estas condiciones generar´an entonces una serie de restricciones que nosotros necesitamos que se verifiquen. Adem´as, una vez sepamos que pueden satisfacerse, nos interesar´a obtener un modelo para tales restricciones, que conformar´a nuestro caso de prueba. Sin embargo, nos encontramos Miguel Garrido Canalejas 2.3. LA HERRAMIENTA Z3 11 (declare-const a Int) (declare-fun f (Int) Bool) (assert (< a 5)) (assert (= (f a) true)) (check-sat) (get-model) Figura 2.4: C´odigo de un programa b´asico en Z3 con el problema de que nosotros deseamos obtener varios casos de prueba y, como hemos comentado anteriormente, Z3 solo nos devuelve un modelo. Para solucionar este problema la t´ecnica que proponemos consiste en ir a˜nadiendo sucesivamente nuevas restricciones que nieguen los modelos obtenidos anteriormente. De este modo, los nuevos modelos tendr´an que verificar ser distintos a los anteriores, obteniendo as´ı diversos casos de prueba. Lenguaje El formato de la entrada en Z3 es una extensi´on del que se define en el SMT-LIB 2.0 standard. Un script de Z3 consta de una secuencia de comandos que se almacenan en una pila que el resolutor gestiona internamente. Entre los comandos podemos encontrar declaraciones de constantes y funciones (declare-const ydeclarefun respectivamente); restricciones (assert), que a˜naden una f´ormula en la pila, y que ser´an las que el verificador trate de hacer ciertas, encontrando una interpretaci´on adecuada para las funciones y constantes declaradas; check-sat, que nos servir´a para determinar si las f´ormulas almacenadas en la pila son satisfactibles o no, devolviendo sat ounsat seg´un corresponda; y get-model que nos devuelve una interpretaci´on para las constantes y funciones en caso de que haya sido resuelto como satisfactible. En la Figura 2.4 puede verse la sintaxis concreta que tendr´ıa un peque˜no programa Z3, en el que quedan recogidos todos los comandos mencionados anteriormente. El verificador tratar´a de dar valores tanto a la constante ay la funci´on fde forma que ambos asertos se hagan ciertos. En caso de encontrar tales valores, nos devolver´a que es satisfactible junto a un modelo concreto, y en caso contrario que es insatisfactible. Queda reflejado en la Figura 2.5 lo obtenido para este sencillo caso de prueba. Se observa que ha encontrado una posible asignaci´on de valores, de modo que el resultado es sat, y que dicha asignaci´on nos conforma un modelo en el que se tiene a=0 yf(x)=true si x=0, o f(x)=true en caso contrario. Trabajo Fin de Grado 12 CAP´ ITULO 2. PRELIMINARES sat (model (define-fun a () Int 0) (define-fun f ((x!0 Int)) Bool (ite (= x!0 0) true true)) ) Figura 2.5: Resultado y modelo de la ejecuci´on del programa de la Figura 2.4 (declare-const a Int) (declare-const b Int) (declare-const c Real) (declare-const d Real) (assert (< (- a 1) (+ b 2))) (assert (>= c d)) (check-sat) (get-model) Figura 2.6: Ejemplo de uso de enteros y reales Teor´ıas Z3 cuenta con resolutores para diversas teor´ıas. Contamos a continuaci´on aquellas que usaremos durante el desarrollo de este trabajo. •Aritm´etica lineal de enteros y reales: declarados mediante el comando declare-const, Z3 nos permite representar y utilizar los n´umeros enteros y reales matem´aticos. Podremos usarlos en nuestras f´ormulas junto a diferentes operadores como +,−, <, etc. (Figura 2.6). Adem´as, Z3 nos da soporte para realizar la divisi´on. •L´ogica proposicional: mediante el tipo predefinido Bool podemos trabajar con expresiones booleanas en Z3. Soporta los operadores usuales and, or, xor, not, =>(para la implicaci´on), ite (que representa la estructura if-then-else) y = (para la doble implicaci´on). En la Figura 2.7 podemos ver un sencillo ejemplo de uso de booleanos con diferentes operadores. Al pedir que la funci´on faplicada al valor true no sea cierta, es decir, que la rama if de dicha funci´on sea falsa, obtenemos los valores de true yfalse para pyqrespectivamente. •Arrays: Z3 cuenta con una teor´ıa b´asica de arrays, representados internamente en forma de funci´on no interpretada de ´ındices en valores, en principio de dominio infinito. Quedan caracterizados mediante dos operaciones, select y Miguel Garrido Canalejas 2.3. LA HERRAMIENTA Z3 13 (declare-const p Bool) (declare-const q Bool) (declare-const r Bool) (define-fun f ((t Bool)) Bool ( ite(= t true) (=> p q) (=> q p) ) ) (assert (not (f true))) (check-sat) (get-model) Figura 2.7: Ejemplo de uso de booleanos store. De este modo, la operaci´on (select a i) nos devuelve el elemento de la posici´on idel array a; y la operaci´on (store a i v) nos devuelve un array id´entico a asalvo en la posici´on ien la que se encuentra el valor v. Cuando queramos un modelo de un array, obtendremos una interpretaci´on del mismo en forma de funci´on, mediante el constructor (- as-array f). Si para un cierto array aobtenemos tal interpretaci´on, entonces para todo ´ındice ise tiene que (select a i) es igual a (f i). Observamos en la Figura 2.8 que Z3 crea la funci´on auxiliar k!0 para dar una interpretaci´on al array arr. Esta funci´on nos devuelve: 5 si recibe un 2; 2 si recibe un 1; y 5 en cualquier otro caso. Esto se ajusta a lo requerido en las dos f´ormulas select. •Tipos algebraicos: encontramos aqu´ı una de las principales ventajas de Z3, que es que nos permitir´a especificar algunas de las estructuras de datos m´as comunes como tuplas, ´arboles o listas. Adem´as, presenta la opci´on de declarar tipos recursivos y mutuamente recursivos. Para declarar un tipo algebraico usaremos el comando declare-datatypes, indicando despu´es las constructoras del tipo. •Cuantificadores: Z3 puede trabajar con f´ormulas que utilicen cuantificadores. Para manejar tales f´ormulas, utiliza diversos enfoques. Al trabajar con cuantificadores, el comando check-sat puede devolvernos un nuevo valor, unknown, en caso de no haber podido instanciar las variables cuantificadas, dado que el problema es en general indecidible. Trabajo Fin de Grado 14 CAP´ ITULO 2. PRELIMINARES (declare-const arr (Array Int Int)) (assert (= (select arr 2) 5)) (assert (= (select arr 1) 2)) (check-sat) (get-model) sat (model (define-fun arr () (Array Int Int) (_ as-array k!0)) (define-fun k!0 ((x!0 Int)) Int (ite (= x!0 2) 5 (ite (= x!0 1) 2 5)) ) Figura 2.8: Declaraci´on de array e interpretaci´on en forma de funci´on Miguel Garrido Canalejas Cap´ıtulo 3 El lenguaje de asertos En un aserto de la IR pueden aparecernos expresiones b´asicas sobre booleanos y enteros, los primeros relacionados entre s´ı mediante los operadores l´ogicos and,or ynot, y los segundos relacionados con operadores como <, =, ≤, etc. Dentro de estas expresiones b´asicas podemos encontrarnos tambi´en cuantificadores (∃y ∀). Pero adem´as, dentro de un aserto podemos encontrarnos predicados y funciones espec´ıficos de ciertos tipos de datos, como podr´ıan ser la longitud de una lista, la ordenaci´on de un array o la altura de un ´arbol. Todos estos asertos quedan reflejados en la Figura 3.1. Durante esta secci´on veremos c´omo transformar predicados a restricciones Z3, y sobre todo, analizaremos c´omo queda definido cada tipo algebraico en Z3 y todas las operaciones que podremos realizar sobre ellos. Pero antes de desarrollar todo ello, es conveniente detenernos en comentar dos aspectos de Z3 que resultan de suma importancia para poder implementar tanto los tipos algebraicos como sus diferentes operaciones. Lo primero, como ya comentamos en la Secci´on 2.3, es la posibilidad de crear tipos recursivos, lo que nos permitir´a crear elementos como los ´arboles o las listas que de otro modo no ser´ıa posible. El segundo aspecto importante es que podremos trabajar con funciones recursivas usando el comando def-fun-rec. Gracias a esta opci´on de Z3, podremos recorrer todas las estructuras recursivas de manera c´omoda haciendo los c´alculos que sean oportunos, que de otro modo, no habr´ıa sido posible. Y es que, por ejemplo, algo tan b´asico como calcular la longitud de una lista requiere el recorrerla recursivamente analizando la constructora y acumulando la longitud. 3.1. Sintaxis b´asica Las expresiones m´as b´asicas que podemos encontrarnos en un aserto, ser´an aquellas que realicen sencillas operaciones sobre enteros o booleanos. Para trabajar con ellas en Z3, bastar´a con crear asertos independientes en los que se vayan plasmando tales operaciones. 15 16 CAP´ ITULO 3. EL LENGUAJE DE ASERTOS φ::= true |false |id {constante booleana o variable } |id t1· · · tn{aplicaci´on de predicado } |φ1∧φ2|φ1∨φ2|φ1→φ2|φ1≡φ2| ¬φ{conectivas proposicionales } | ∀ idi:typei. φ | ∃ idi:typei. φ {aserto cuantificado } Figura 3.1: Sintaxis abstracta de los asertos (assert (and p q)) (assert (not (and p (or q r))) (assert (=> p (and q r)) Figura 3.2: Ejemplos sobre expresiones booleanas Al trabajar con expresiones booleanas, podremos encontrarnos distintas variables de tipo Bool relacionadas entre s´ı mediante operadores l´ogicos tales como and,or,not, implicaciones, etc. Todas estos operadores est´an a nuestra disposici´on en la plataforma Z3, por lo que podemos utilizarlos con total normalidad como har´ıamos en cualquier otro lenguaje. Se muestran en la Figura 3.2 algunos ejemplos sencillos sobre asertos con booleanos, donde las variables p,qyrson de tipo Bool. Por su parte, con los asertos que impliquen enteros podremos encontrarnos operaciones como sumas, restas, multiplicaciones o divisiones, as´ı como relaciones de orden tales como ≤, =, etc. De nuevo, todos estos operadores est´an a nuestra disposici´on en Z3 por lo que nuestros asertos podr´an incluirlos sin problema alguno. Algunos ejemplos sencillos pueden verse en la Figura 3.3, donde aybson variables enteras. Adem´as de estas operaciones b´asicas sobre enteros, podremos encontrarnos, tanto en los asertos como en funciones que iremos exponiendo a lo largo de la secci´on, otras funciones para las que Z3 no nos da soporte y tenemos que definirlas nosotros. Se trata de operaciones para encontrar el m´aximo o m´ınimo de dos n´umeros (Figuras 3.4 y 3.5 respectivamente) y para obtener el valor absoluto de un cierto n´umero (Figura 3.6). 3.2. Tipo Lista Para definir una lista lo haremos de forma recursiva siguiendo la idea de que una lista es un elemento seguido de otra lista. As´ı, las listas quedan definidas en Z3 como puede verse en la Figura 3.7. Se observa que las constructoras son bien nil, para la lista vac´ıa, bien cons para una lista no vac´ıa. En este segundo caso, siguiendo la idea comentada previamente, tenemos un elemento de tipo Int que ser´a la cabeza de la lista y una cola que ser´a otra lista. Para acceder a estos dos campos contamos con los destructores hd ytl. Definido ya el tipo, queda ver cada una de las operaciones que podremos realizar sobre ´el. En los asertos, entre los predicados que refieren a listas nos enMiguel Garrido Canalejas 3.2. TIPO LISTA 17 (assert (= a 5)) (assert (> (+ a b) 7) Figura 3.3: Ejemplos sobre expresiones con enteros (define-fun max ((a Int) (b Int)) Int (ite(> a b) a b) ) Figura 3.4: C´alculo del m´aximo de dos n´umeros contramos: length, para calcular la longitud de una lista; member, que nos permite saber si un elemento pertenece a una lista; sortedList, para saber si una lista est´a ordenada; y multiset, que nos proporciona el multiset de la lista. Veamos entonces como queda implementada cada una de ellas en Z3. Longitud La operaci´on length, nos devolver´a la longitud de una lista dada. El c´alculo de dicha longitud se har´a de forma recursiva como puede verse en la Figura 3.8. Se observa que la longitud ser´a cero si la lista es vac´ıa o bien uno m´as la longitud de la lista que conforma la cola. Lista ordenada Con esta operaci´on comprobaremos si una cierta lista est´a ordenada o no, devolviendo true ofalse respectivamente. De nuevo, esta funci´on se define recursivamente, de manera que una lista est´a ordenada si se cumple que el elemento de la cabeza de la lista es menor que el elemento de la cabeza de la cola y, tambi´en, que la cola est´e ordenada. Adem´as, tanto una lista vac´ıa como una lista con un ´unico elemento est´an ordenadas. Esta idea queda reflejada en el c´odigo de la Figura 3.9, en la que el primer ite considera el caso de la lista vac´ıa, el segundo considera la lista de un solo elemento, y la parte del else se ocupa del c´alculo recursivo. Pertenencia Nos encontramos de nuevo con una funci´on recursiva, que nos devolver´a true en caso de que un elemento dado pertenezca a una lista tambi´en dada o false en caso contrario. Un elemento pertenecer´a a una lista, bien si es la cabeza de la misma o bien si pertenece a la cola. Obviamente, un elemento no puede pertenecer a una lista vac´ıa, por lo que el caso b´asico de nuestra funci´on en el que la lista sea Trabajo Fin de Grado 24 CAP´ ITULO 3. EL LENGUAJE DE ASERTOS (define-fun lengthArr ((a (Arr Int))) Int (second a) ) Figura 3.17: Longitud de un array (define-fun sortedArr ((a (Arr Int)) (b1 Int) (b2 Int)) Bool ( forall ((i Int) (j Int)) (=> (and (<= b1 i) (<= i j) (< j b2)) (<= (select (first a) i) (select (first a) j))) ) ) Figura 3.18: Array ordenado Altura Para calcular la altura de un ´arbol lo haremos de forma recursiva, seg´un queda definido en la Figura 3.23. Dado un cierto ´arbol, la funci´on nos devolver´a la altura del mismo. Calcularemos la altura como uno m´as el m´aximo de las alturas de los hijos izquierdo y derecho. En caso de tener un ´arbol vac´ıo, la altura es cero. As´ı, si por ejemplo tenemos un ´arbol con un solo nodo, vemos que obtendr´ıamos altura uno (1 + max(0,0)), como cabr´ıa esperar. Para la llamada recursiva, vemos que llamamos a la funci´on height pas´andole como par´ametro el resultado de aplicar la constructora izq oder, que es de tipo Tree, tal y como espera la funci´on. Altura m´ınima La altura m´ınima de un ´arbol binario es la altura o profundidad desde la ra´ız hasta el nodo vac´ıo m´as cercano. Es decir, es igual que la altura excepto que debemos buscar el m´ınimo de las alturas de los hijos en vez del m´aximo. La definici´on en Z3 (Figura 3.24) es, por tanto, an´aloga a la funci´on height, salvo que en el caso recursivo, en vez de coger el m´aximo entre las alturas de los hijos, como hac´ıamos en esa funci´on, aqu´ı tendremos que coger el m´ınimo. Cardinal Cuando hablamos del cardinal de un ´arbol binario nos referimos al n´umero de elementos que tiene. Es decir, cuantos nodos no vac´ıos, o lo que es lo mismo, que la constructora no sea leaf, nos encontramos. As´ı, el cardinal de un nodo vac´ıo ser´a Miguel Garrido Canalejas 3.4. TIPO ´ ARBOL BINARIO 25 (define-fun-rec sortedArr ((a (Arr Int)) (b1 Int) (b2 Int)) Bool ( ite(>= b1 b2) true (and (<= (select (first a) b1) (select (first a) (+ b1 1))) (sortedArr a (+ b1 1) b2)) ) ) Figura 3.19: Funci´on recursiva para arrays ordenados (define-fun multisetArr ((a (Arr Int))) (Multiset Int) (multisetArrAux 0 a) ) (define-fun-rec multisetArrAux ((i Int) (a (Arr Int))) (Multiset Int) ( ite(= i (second a)) emptyMs (Mset-union (multisetArr (+ i 1) a) (unitMs (select (first a) i))) ) ) Figura 3.20: Funciones para calcular el multiset de un array cero y el de uno no vac´ıo ser´a uno. Esto queda reflejado con la funci´on recursiva card de la Figura 3.25, en la que en el caso base en el que el ´arbol es vac´ıo devuelve cero, y en el caso recursivo hace la suma de los cardinales de cada uno de los hijos para calcular el resto de nodos y le suma uno por el nodo actual. Set Dado un ´arbol, podemos estar interesados en obtener una representaci´on del mismo en forma de Set. El primer inconveniente que nos encontramos es la representaci´on de sets en Z3, pues no cuenta con un tipo propio. La forma elegida para tratarlos es como un array de valores de tipo T en booleanos, donde T es el mismo tipo que el de los valores del ´arbol (Figura 3.26), de modo que si un cierto valor vest´a en el conjunto, arr[v]=true. Solucionada la representaci´on del tipo, queda resolver como pasar los valores que nos encontremos en el ´arbol al array. Lo hacemos recursivamente de modo que el set de un ´arbol es la uni´on de los sets obtenidos para sus dos hijos, unido a su vez al conjunto unitario formado por el elemento del nodo en el que estemos. Como caso Trabajo Fin de Grado 26 CAP´ ITULO 3. EL LENGUAJE DE ASERTOS (define-fun permut ((a1 (Arr Int)) (a2 (Arr Int))) Bool (= (multisetArr (first a1)) (multisetArr (first a2))) ) Figura 3.21: Comprobaci´on de si dos arrays son permutaci´on el uno del otro (declare-datatypes (T) ((Tree leaf (node (val T) (izq Tree) (der Tree))))) Figura 3.22: Definici´on del tipo ´arbol binario base tendremos el ´arbol vac´ıo para el cual deberemos devolver un conjunto tambi´en vac´ıo. Por tanto, antes de definir la funci´on Set nos hace falta definir las funciones auxiliares empty, que nos devuelve un set vac´ıo (Figura 3.27); union, que hace la uni´on de dos sets (Figura 3.28); y unit, que se encarga de crear un conjunto con un ´unico elemento (Figura 3.29). La primera de ellas simplemente inicializa un array con todas sus posiciones a false. La segunda, gracias al map aplica la operaci´on or a cada par de elementos de dos arrays dados, es decir, ∀i∈T:set[i] = set1[i]∨set2[i]. La tercera pone a true la posici´on dada de un array vac´ıo. Vistas ya entonces todas las funciones auxiliares, solo queda ver c´omo queda la funci´on que obtiene el set de un ´arbol. Si el ´arbol es vac´ıo, devolver´a un array vac´ıo usando la funci´on empty. Si, por el contrario, el ´arbol no es vac´ıo, y estamos en un nodo con valor ve hijos izquierdo y derecho lyr, respectivamente, devolveremos: set(l)∪unit(v)∪set(r). Todo esto queda reflejado en la Figura 3.30. BST Un ´arbol binario es de b´usqueda si todos los nodos del hijo izquierdo son menores que la ra´ız, y ´esta a su vez es menor que los nodos del hijo derecho. Adem´as, ambos hijos izquierdo y derecho deben preservar tambi´en esta propiedad. As´ı, para comprobar si un ´arbol es un BST tendremos que hacerlo de forma recursiva. Comprobar que el orden de los elementos es el adecuado no puede limitarse a comparar la ra´ız de un ´arbol con los valores almacenados en los hijos izquierdo y derecho, pues lo que necesitamos es que todos los nodos verifiquen la propiedad. Usamos entonces, para hacer las comprobaciones, el set de los hijos, de modo que todo elemento del set del hijo izquierdo deber´a ser menor que la ra´ız, y todo elemento del set del hijo derecho deber´a ser mayor. De este modo, la funci´on har´ıa uso del forall de Z3, a fin de comprobar la propiedad mencionada para todos los elementos de cada uno de los sets. No obstante, con esta funci´on esperamos obtener dos funcionalidades. La primera de ellas, comprobar si un ´arbol dado es BST. Para este caso, la definici´on aportada para nuestra funci´on es perfectamente v´alida. La segunda de las funcioMiguel Garrido Canalejas 3.4. TIPO ´ ARBOL BINARIO 27 (define-fun-rec height ((t (Tree Int))) Int ( ite(= t leaf) 0 (+ 1 (max (height (izq t)) (height (der t)))) ) ) Figura 3.23: Operaci´on height sobre un ´arbol binario (define-fun-rec minHeight ((t (Tree Int))) Int ( ite(= t leaf) 0 (+ 1 (min (minHeight (izq t)) (minHeight (der t)))) ) ) Figura 3.24: Altura m´ınima de un ´arbol nalidades que esperamos conseguir, a partir de esta funci´on, es la de rellenar una cierta estructura de ´arbol con valores cumpliendo que el ´arbol resultante sea BST. Aqu´ı sin embargo encontramos m´as problemas con nuestra definici´on, puesto que al trabajar con cuantificadores Z3 no es capaz de instanciar correctamente las variables de la estructura de manera que respeten las condiciones impuestas. Por ello, debemos redefinir la funci´on sin usar el cuantificador ni sets. Consideremos la estructura general de un ´arbol binario como en la Figura 3.31. Tal ´arbol ser´a BST si se verifica que res mayor que el valor m´ınimo de t1y menor que el m´aximo de t2. Por tanto, lo primero que necesitamos es definirnos en Z3 dos funciones que se encarguen de calcular los valores m´ınimo y m´aximo de un cierto ´arbol. Explicamos la funci´on que calcula el m´ınimo y la encargada de calcular el m´aximo es totalmente an´aloga. Dado un ´arbol, para encontrar el m´ınimo queremos ir recorriendo recursivamente los hijos izquierdo y derecho y comparando los valores almacenados en los nodos de estos con el valor almacenado en la ra´ız. De este modo, cuando lleguemos a un nodo vac´ıo le asignaremos un valor suficientemente grande, y en caso de estar en un nodo no vac´ıo devolveremos el m´ınimo entre el valor almacenado en dicho nodo y el valor m´ınimo de los ´arboles que conforman sus dos hijos. Esta idea queda plasmada en la funci´on de la Figura 3.32 y en la funci´on equivalente para calcular el m´aximo (Figura 3.33). Conocidos ya el m´ınimo y el m´aximo de los dos hijos de un nodo, podemos aplicar la idea comentada para averiguar si es BST y descender recursivamente por los hijos comprobando si ´estos lo son tambi´en. As´ı, la Figura 3.34 recoge la funci´on encargada de comprobar si un ´arbol pasado como par´ametro es o no de b´usqueda. Trabajo Fin de Grado 28 CAP´ ITULO 3. EL LENGUAJE DE ASERTOS (define-fun-rec card ((t (Tree Int))) Int ( ite(= t leaf) 0 (+ 1 (+ (card (izq t)) (card (der t)))) ) ) Figura 3.25: Cardinal de un ´arbol (define-sort Set (T) (Array T Bool)) Figura 3.26: Definici´on del tipo Set Mont´ıculo Un mont´ıculo es una particularizaci´on de los ´arboles binarios, donde el problema que pretende resolverse es el de encontrar el elemento m´ınimo o m´aximo, seg´un corresponda, y no un elemento cualquiera. Seg´un el elemento que desee encontrarse tenemos los minHeaps, en los que hay acceso directo al elemento m´ınimo, y los maxHeaps, en los que lo hay al m´aximo. Nosotros trabajaremos con los primeros. En un minHeap, la caracter´ıstica fundamental es que todos los hijos de un nodo son mayores o iguales que ´este, pero luego entre ellos no hay ninguna restricci´on adicional. Esto queda reflejado en la funci´on de la Figura 3.35, en la que se comprueba recursivamente que se verifique esta propiedad. En el primer if consideramos el caso en el que el ´arbol sea vac´ıo y en el segundo tenemos que el ´arbol est´a formado por un ´unico nodo, cumpli´endose en ambos casos que el ´arbol t es un mont´ıculo y devolviendo por tanto true. En el tercer if consideramos que solo uno de los hijos sea vac´ıo, concretamente el izquierdo, de modo que en esa rama solo tenemos que comprobar los valores de la ra´ız y del hijo derecho, mientras que en el cuarto hacemos lo mismo pero considerando esta vez que el hijo vac´ıo es el derecho. Por ´ultimo, en la rama del else final encontramos el caso en que ambos hijos sean no vac´ıos, para el cual debemos hacer todas las comprobaciones entre el valor de la ra´ız y los de los hijos. Por otro lado, un mont´ıculo sesgado requiere haber sido formado mediante dos mont´ıculos sesgados previos usando mezcla sesgada. Esta propiedad resulta imposible de especificar en Z3, y tampoco nos resulta de gran inter´es, por ello, consideraremos, como ´unica restricci´on de este tipo de mont´ıculos, la que refiere al orden de sus elementos como en el resto de mont´ıculos. Por tanto, nos bastar´a con comprobar la funci´on de la Figura 3.35 para afirmar si un mont´ıculo es sesgado. Miguel Garrido Canalejas 3.5. TIPO ´ ARBOL AVL 29 (define-fun empty () (Set Int) ((as const (Array Int Bool)) false)) Figura 3.27: Funci´on empty (define-fun set-union ((s1 (Set Int)) (s2 (Set Int))) (Set Int) ((_ map or) s1 s2 ) ) Figura 3.28: Funci´on union Zurdo Uno de los tipos de mont´ıculos m´as interesantes que nos encontramos son los mont´ıculos zurdos. Para la definici´on de un mont´ıculo zurdo es necesario usar la altura m´ınima definida previamente en esta secci´on. Un mont´ıculo es zurdo entonces si es vac´ıo, o si ambos hijos son zurdos y adem´as la altura m´ınima del hijo izquierdo es mayor o igual que la del hijo derecho. Esta idea queda reflejada en Z3 en la funci´on recursiva de la Figura 3.36. Por tanto, un mont´ıculo debe cumplir, para ser zurdo, tanto la funci´on anterior isHeap, como esta, zurdo. 3.5. Tipo ´ Arbol AVL Un ´arbol AVL es un tipo especial de ´arbol binario en el que en cada nodo, adem´as de almacenar un cierto valor, guardamos tambi´en la altura a la que se encuentra dicho nodo en el ´arbol. Por ello, la representaci´on en Z3 es totalmente id´entica a la de los ´arboles binarios, pero a˜nadiendo simplemente un campo m´as a la constructora node que refiera a la altura del nodo (Figura 3.37). Adem´as, los ´arboles AVL son ´arboles de b´usqueda, por lo que los elementos deber´an mantener un cierto orden, pero cuentan con una caracter´ıstica adicional, que es que la altura debe mantener el ´arbol equilibrado, esto es, la diferencia entre las alturas de los dos hijos de un nodo cualquiera no puede ser mayor que uno. La mayor´ıa de los c´omputos que necesitemos realizar sobre un AVL ser´an los mismos que hac´ıamos con los ´arboles binarios: calcular la altura mediante una funci´on height; calcular el n´umero de elementos o cardinal; y averiguar su set. Adem´as de estas funciones ya conocidas, que deber´an ser redefinidas para el tipo AVL, aparece una nueva funci´on, isAVL, encargada de comprobar que se verifiquen todas las condiciones necesarias para que un ´arbol binario sea un AVL. Trabajo Fin de Grado 30 CAP´ ITULO 3. EL LENGUAJE DE ASERTOS (define-fun unit ((i Int)) (Set Int) (store empty i true)) Figura 3.29: Funci´on unit (define-fun-rec set ((t (Tree Int))) (Set Int) ( ite(= t leaf) empty (set-union (set-union (set (izq t)) (set (der t))) (unit (val t))) ) ) Figura 3.30: Funci´on que calcula el set de un ´arbol binario Altura Calcular la altura de un ´arbol AVL respeta la idea seguida con los ´arboles binarios. A saber, la altura de un nodo ser´a uno m´as el m´aximo de las alturas de sus dos hijos. Por ello, la definici´on de la funci´on queda exactamente igual que estaba para tales ´arboles, con la ´unica salvedad de que hay que renombrar las constructoras. En la Figura 3.38 queda reflejada esta funci´on. Cardinal Del mismo modo que con la altura, calcular el cardinal es igual para los ´arboles AVL que para los binarios. Por ello, la funci´on de la Figura 3.39, encargada de hacer tal c´alculo, queda definida del mismo modo que la de la Figura 3.25 renombrando las constructoras que aparezcan. Set Una vez m´as, nos encontramos con una funci´on que no presenta diferencias con la utilizada para ´arboles binarios, m´as all´a de los renombramietos oportunos. Calcular el set de un ´arbol AVL se hace del mismo modo que con ´arboles binarios, es decir, si tenemos un ´arbol vac´ıo el conjunto devuelto es tambi´en vac´ıo, y para un nodo no vac´ıo el conjunto se obtiene de realizar la uni´on entre los sets de los dos hijos y el conjunto unitario formado por el valor almacenado en dicho nodo. Por ello, se har´a uso aqu´ı tambi´en de las funciones auxiliares definidas para los ´arboles binarios, a saber, empty (Figura 3.27), unit (Figura 3.29), y set-union (Figura 3.28). La funci´on general que calcula el set del ´arbol queda definida en la Figura 3.40. Miguel Garrido Canalejas 3.5. TIPO ´ ARBOL AVL 31 Figura 3.31: Estructura general de un ´arbol binario (define-fun-rec minT ((t (Tree Int))) Int ( ite(= t leaf) 2000 (min (val t) (min (minT (izq t)) (minT (der t)))) ) ) Figura 3.32: C´alculo del valor m´ınimo de un ´arbol BST Para que un ´arbol sea AVL tendr´a que cumplir que sea de b´usqueda. Por ello, necesitamos redefinir el predicado isBST de la Figura 3.34. La idea seguida es la misma, pues los elementos deben mantener el mismo orden que impon´ıamos en tal funci´on. Por tanto, ´unicamente debemos preocuparnos de renombrar las funciones auxiliares (Figura 3.41 y Figura 3.42) y modificar, tanto en ellas como en la principal (Figura 3.43), las diferentes apariciones de las constructoras de nuestro tipo de datos. AVL Como coment´abamos al principio de la secci´on, un ´arbol AVL no deja de ser un ´arbol binario de b´usqueda, con la ´unica particularidad de que tiene una cierta imposici´on sobre las alturas. Ser´an entonces estas las restricciones que debamos comprobar a la hora de determinar si un cierto ´arbol es o no un AVL. En primer lugar, por ser un ´arbol de b´usqueda tendremos que recurrir al predicado isBST que nos determina si el orden de los elementos en los nodos es el adecuado. En segundo lugar, hay que comprobar que la diferencia de alturas entre ambos hijos no sea mayor que uno. Por ´ultimo, para que un cierto ´arbol sea Trabajo Fin de Grado 32 CAP´ ITULO 3. EL LENGUAJE DE ASERTOS (define-fun-rec maxT ((t (Tree Int))) Int ( ite(= t leaf) -2000 (max (val t) (max (maxT (izq t)) (maxT (der t)))) ) ) Figura 3.33: M´aximo de un ´arbol (define-fun-rec isBST ((t (Tree Int))) Bool ( ite(= t leaf) true (ite (and (= (izq t) leaf) (= (der t) leaf)) true (ite (= (izq t) leaf) (and (isBST (der t)) (< (val t) (minT (der t)))) (ite (= (der t) leaf) (and (isBST (izq t)) (< (maxT (izq t)) (val t))) (and (and (isBST (izq t)) (isBST (der t))) (and (< (maxT (izq t)) (val t)) (< (val t) (minT (der t))))) ) ) ) ) ) Figura 3.34: Funci´on que comprueba si un ´arbol es BST AVL, adem´as de cumplir estas dos condiciones anteriores, tiene que cumplir tambi´en que sus dos hijos sean tambi´en AVL. Por ello, la comprobaci´on deber´a hacerse de manera recursiva, considerando como caso base el ´arbol vac´ıo, el cual s´ı es AVL. La funci´on de la Figura 3.44 plasma todas estas ideas. Observamos que en la rama if comprobamos si el ´arbol es vac´ıo, devolviendo true en tal caso, y que en la rama del else hacemos las llamadas recursivas con los hijos izquierdo y derecho como par´ametros, adem´as de comprobar que sea BST y que se cumpla la diferencia de alturas requerida, siendo absol la funci´on valor absoluto definida como en la Secci´on 3.1 de este cap´ıtulo. Adem´as de todo esto, tenemos que a˜nadir una condici´on especial. Si recordamos la definici´on de un ´arbol AVL, ten´ıamos un campo reservado en cada nodo para almacenar su altura. Pues bien, este valor debe ser correcto, es decir, debe ser efectivamente la altura de dicho nodo. Por ello, al comprobar que un ´arbol sea AVL haremos tambi´en tal comprobaci´on, lo que se reduce a ver si el valor guardado en el nodo es igual a uno m´as el m´aximo de las alturas de sus hijos. Miguel Garrido Canalejas 3.5. TIPO ´ ARBOL AVL 33 (define-fun-rec isHeap ((t (Tree Int))) Bool ( ite(= t leaf) true (ite (and (= (izq t) leaf) (= (der t) leaf)) true (ite(= (izq t) leaf) (and (< (value t) (minT (der t))) (isHeap (der t))) (ite(= (der t) leaf) (and (< (value t) (minT (izq t))) (isHeap (izq t))) (and (and (< (val t) (val (izq t))) (< (val t) (val (der t)))) (and (isHeap (izq t)) (isHeap (der t)))) ) ) ))) Figura 3.35: Funci´on isHeap (define-fun-rec isLeftist ((t (Tree Int))) Bool ( ite (= t leaf) true (and (and (isLeftist (izq t)) (isLeftist (der t))) (>= (minHeight (izq t)) (minHeight (der t)))) ) ) Figura 3.36: Funci´on que comprueba si un ´arbol binario es zurdo Esta funci´on es la principal de los ´arboles AVL y nos proporcionar´a dos usos fundamentales. El primero y m´as b´asico es comprobar si el ´arbol que recibe como par´ametro verifica todas las condiciones que debe cumplir para ser AVL. No obstante, el uso m´as interesante es rellenar una cierta estructura de forma que el ´arbol resultante sea AVL. De este modo, un cierto ´arbol con estructura de AVL, pero con variables desconocidas como campos de cada uno de los nodos, puede pasarse a la funci´on como par´ametro y que ´esta nos de valores a cada una de las variables, tanto las de valor como las de altura, cumpliendo todas ellas todos los requisitos necesarios. Trabajo Fin de Grado 40 CAP´ ITULO 3. EL LENGUAJE DE ASERTOS (define-fun-rec cardL ((t (LLRB Int))) Int ( ite(= t leafL) 0 (+ 1 (+ (cardL (izq t)) (cardL (der t)))) ) ) Figura 3.49: Cardinal de un ´arbol rojinegro (define-fun-rec setL ((t (LLRB Int))) (Set Int) ( ite(= t leafL) empty (set-union (set-union (setL (izq t)) (setL (der t))) (unit (val t))) ) ) Figura 3.50: Obtenci´on del set de un LLRB de la funci´on goodColor. 3.7. Doble uso de los predicados Durante la explicaci´on de algunos de los m´etodos ya hemos ido introduciendo la idea de que presentaban dos modos de uso. Este planteamiento requiere abordarlo con algo m´as de detenimiento pues es lo m´as innovador que nos aporta este trabajo. Si recordamos, en cap´ıtulos previos dec´ıamos que hasta ahora la generaci´on de casos de prueba consist´ıa en generar diferentes casos y filtrarlos descartando aquellos que no eran v´alidos, y que nosotros tratar´ıamos de generarlos siendo directamente buenos. Pues bien, es precisamente este doble uso de los predicados definidos el que nos permite hacer esto sin perder la capacidad de filtrar en caso de necesitarlo. En primer lugar, el uso m´as b´asico que podemos hacer es el de filtrar de manera cl´asica. Dado un cierto valor para una variable, cualquiera que sea su tipo, podremos llamar a una cierta funci´on que nosotros tengamos definida que realice una serie de comprobaciones sobre ella y nos diga si cumple una serie de condiciones o no. Hasta aqu´ı, no encontramos nada nuevo, puesto que esto puede hacerse con cualquier funci´on que nos definamos en cualquier lenguaje de programaci´on. En segundo lugar, podemos usar los predicados de Z3 para asignar valores a variables cumpliendo una serie de condiciones. Y es aqu´ı donde se nos presentan las opciones m´as novedosas e interesantes, pues, estamos entonces en condiciones Miguel Garrido Canalejas 3.7. DOBLE USO DE LOS PREDICADOS 41 (define-fun goodColor ((t (LLRB Int))) Bool ( ite(= t leafL) true (ite(= (color t) Negro) (=> (= (getColor (der t)) Rojo) (= (getColor (izq t)) Rojo)) (and (= (getColor (izq t)) Negro) (= (getColor (der t)) Negro)) ) ) ) Figura 3.51: Funci´on goodColor para ´arboles rojinegros (define-fun getColor ((t (LLRB Int))) Bool ( ite(= t leafL) Negro (color t) ) ) Figura 3.52: Funci´on getColor para ´arboles rojinegros de darle directamente valores buenos a una variable, en lugar de perder recursos en asignarle valores aleatorios y luego comprobar si nos valen o no. Por ejemplo, de manera muy sencilla, si una cierta variable var necesitamos que sea menor que tres, con el primer enfoque tendr´ıamos que darle valores aleatorios y luego descartar mientras que con el segundo podemos conseguir que autom´aticamente tome un valor que nos interese. Esto que podr´ıa parecer irrelevante con variables y restricciones tan sencillas, puede aplicarse a cualquier variable de cualquier tipo, y es ah´ı donde obtenemos la verdadera potencia de este m´etodo de utilizaci´on de nuestros predicados. Consideremos por ejemplo una cierta variable de tipo Tree. Esta variable tiene cinco nodos para los que necesitamos obtener unos valores que nos verifiquen una serie de restricciones de orden, por ejemplo, que est´en ordenadas de manera que el ´arbol sea de b´usqueda. Si solo cont´aramos con el primer m´etodo de uso comentado, tendr´ıamos que limitarnos a crear ´arboles de cinco nodos con valores aleatorios en cada uno de ellos, y pasarlos por nuestro m´etodo correspondiente para comprobar si est´an ordenados como dese´abamos. No obstante, con la segunda posibilidad podemos almacenar en cada nodo una cierta variable, de modo que al pedirle a Z3 que verifique la funci´on correspondiente, ´el solo sea capaz de darnos valores buenos para cada uno de estos nodos ahorr´andonos tanto la generaci´on autom´atica como el filtrado. No obstante, se encuentran algunas limitaciones en este modo de uso. Y es Trabajo Fin de Grado 42 CAP´ ITULO 3. EL LENGUAJE DE ASERTOS (define-fun-rec isBSTL ((t (LLRB Int))) Bool ( ite(= t leafL) true (ite (and (= (izq t) leafL) (= (der t) leafL)) true (ite (= (izq t) leafL) (and (isBSTL (der t)) (< (val t) (minTL (der t)))) (ite (= (der t) leafL) (and (isBSTL (izq t)) (< (maxTL (izq t)) (val t))) (and (and (isBSTL (izq t)) (isBSTL (der t))) (and (< (maxTL (izq t)) (val t)) (< (val t) (minTL (der t))))) ) ) ) ) ) Figura 3.53: Funci´on que comprueba si un ´arbol rojinegro es de b´usqueda (define-fun-rec isLlrbAux ((t (LLRB Int))) Bool ( ite(= t leafL) true (and (isBSTL t) (and (and (and (isLlrbAux (izq t)) (isLlrbAux (der t))) (goodColor t)) (eq (blackHeight (izq t)) (blackHeight (der t))))) ) ) Figura 3.54: Funci´on isLlrbAux que, a la hora de crear variables de un tipo algebraico perdemos esta potencia. Por ejemplo, tal y como hemos visto, funciones como la encargada de calcular el cardinal de un ´arbol o la altura del mismo, est´an definidas de manera recursiva. Por ello, si nosotros pidi´eramos a Z3 que intentara darle valor a una variable tde tipo Tree, que es un tipo algebraico definido tambi´en recursivamente, cumpliendo que tuviera un cierto cardinal o una cierta altura, Z3 es incapaz de encontrar una asignaci´on para nuestra variable t. Por ello, para estos tipos de restricciones no nos quedar´a m´as remedio que tratarlas con el primero de los enfoques comentados. Ser´a durante el cap´ıtulo pr´oximo cuando entremos en detalle a comentar como hemos decidido resolver estas limitaciones, intentando exprimir la potencia de Z3 al m´aximo cuando sea posible, clasificando las restricciones en diferentes tipos. Comentaremos tambi´en a qu´e tipo de restricciones pertenecen cada una de las funciones vistas a lo largo de este cap´ıtulo y con ello el enfoque de uso que les damos. Miguel Garrido Canalejas 3.7. DOBLE USO DE LOS PREDICADOS 43 (define-fun isLlrb ((t (LLRB Int))) Bool ( and (= (getColor t) Negro) (isLlrbAux t) ) ) Figura 3.55: Funci´on isLlrb A modo de conclusi´on, se incluye un peque˜no ejemplo con el que ilustrar estas ideas que acabamos de comentar. Supongamos que tenemos una variable tque es un ´arbol binario (tipo Tree). Abordemos primero las limitaciones. Si pedimos a Z3 que trate de verificar una restricci´on del estilo (assert (= (card t) 4)), en la que se requiere que el cardinal de tsea cuatro, nos encontramos que Z3 se queda bloqueado, incapaz de resolver este problema. Comentamos ahora los diferentes modos de uso. Mantengamos la misma variable t, pero esta vez con una estructura ya definida, por ejemplo (node x1 (node x2 leaf leaf) (node x3 leaf leaf)), donde cada variable xirefiere al valor almacenado en cada nodo. Si le pedimos a Z3 que verifique la restricci´on (assert (= (card t) 3)), en la que se le pide que el cardinal sea tres, actuar´a en modo de filtro calculando el cardinal de nuestro ´arbol y devolvi´endonos sat ounsat seg´un cumpla la restricci´on o no. Por otro lado, si utilizamos una restricci´on del tipo (assert (isBST t)), estamos pidiendo a Z3 que verifique que el ´arbol es de b´usqueda. Pues bien, es aqu´ı donde entra en juego el segundo modo de uso, pues Z3 no solo nos devuelve sat en caso de que pueda rellenarse, sino que nos devuelve tambi´en valores para cada variable xi, a saber, x1= 1999, x2=−1999 yx3= 2001. Estos valores son aleatorios pero cumplen el orden requerido. Trabajo Fin de Grado 44 CAP´ ITULO 3. EL LENGUAJE DE ASERTOS Miguel Garrido Canalejas Cap´ıtulo 4 Estrategia de generaci´on de casos Como ya hemos mencionado, este trabajo tiene por objetivo la generaci´on de casos de prueba que se ajusten autom´aticamente a las precondiciones del programa que deseemos probar. Para ello, resulta conveniente transformar tales precondiciones en una secuencia de restricciones. As´ı, con estas restricciones y gracias a la potencia de Z3, podremos obtener un modelo que cumpla todas ellas, es decir, un caso de prueba de nuestro programa totalmente v´alido. Para poder generar los casos de prueba correctamente, en primer lugar hemos tenido que clasificar las restricciones que puede interesarnos tratar en diferentes grupos, como veremos en la primera secci´on de este cap´ıtulo. Una vez determinadas las diferentes restricciones y elegido el m´etodo seguido para tratar cada una de ellas, solo queda transformar la IR a un conjunto de restricciones procesables por Z3, creando para ello un archivo de formato smt. Comentaremos, por tanto, en la segunda secci´on de este cap´ıtulo la estrategia seguida para llevar este proceso a cabo. Hablaremos tambi´en de las limitaciones encontradas y como las hemos ido solventando. 4.1. Tipos de restricciones Como ya se introdujo en la Secci´on 3.7, las diferentes funciones de Z3 pod´ıan ser utilizadas de diversas maneras, encontr´andonos problemas cuando quer´ıamos construir un elemento de tipo algebraico a partir de una altura o un n´umero de elementos. Estas funciones se utilizar´an por precondiciones que puedan requerirlas. Por tanto, estas diferencias entre m´etodos de utilizaci´on de unas funciones y otras deriva en que debemos tratar de manera diferente los asertos que podamos encontrarnos en las precondiciones. Cada aserto al final impone un restricci´on sobre una cierta variable, por lo que lo que haremos es clasificar las restricciones en tres grandes grupos: restricciones de tama˜no, restricciones de estructura y restricciones de contenido. 45 46 CAP´ ITULO 4. ESTRATEGIA DE GENERACI´ ON DE CASOS 4.1.1. Restricciones de tama˜no Tal y como su nombre indica, hacen referencia al tama˜no de las diferentes estructuras que puedan aparecernos. Ser´an entonces la funci´on lengthArr para arrays, length para listas y card para ´arboles. Para arrays, si recordamos, la longitud no era m´as que un campo de una tupla, por lo que no habr´ıa m´as que crearnos una restricci´on para asignar el valor deseado a tal campo y tendr´ıamos ya la longitud del array. No obstante, para listas y ´arboles, que son tipos algebraicos, nos encontramos el problema mencionado en la Secci´on 3.7, a saber, Z3 no puede crear una estructura a partir de un cierto tama˜no. Por ello, estas funciones ser´an tratadas como meros elementos de verificaci´on y no para crear variables. De esta manera, podremos utilizarlas para comprobar si el tama˜no de una estructura es el requerido, en caso de que la precondici´on nos lo pida. 4.1.2. Restricciones de estructura Aplicadas exclusivamente a ´arboles, trabajar´an sobre la estructura de los mismos, es decir, sobre aspectos como la altura, la altura m´ınima, los colores, la altura negra... Con estas restricciones desear´ıamos obtener ´arboles vac´ıos, es decir, que no tengan ning´un dato almacenado, y que se ajusten a la estructura pedida. Por ejemplo, supongamos una cierta precondici´on que nos pide que la diferencia de alturas entre los hijos izquierdo y derecho de un ´arbol no sea mayor que uno (condici´on interna de ser AVL), nos gustar´ıa que Z3 nos construyera un ´arbol adecuado a esto. Es decir, pedirle a Z3 que nos resuelva una f´ormula del estilo (assert (= (difHeight t) true)), siendo difHeight una supuesta funci´on que compruebe la condici´on sobre las alturas mencionada anteriormente, y tuna constante del tipo Tree definido como en la Secci´on 3.4, y que nos construya directamente tcomo nosotros queremos. Pues bien, nos enfrentamos de nuevo a la limitaci´on comentada de Z3, puesto que no es capaz de realizar tal tarea. Vistos entonces los problemas encontrados con este tipo de asertos, veamos c´omo tratarlos para salvar estas dificultades. Como ya hac´ıamos con las restricciones de tama˜no, nos limitaremos a tratar estas restricciones como elementos de verificaci´on. De este modo, s´ı podremos verificar que un ´arbol verifique que cumple alguna cierta propiedad estructural. Las restricciones estructurales acostumbran a venir incluidas dentro de predicados m´as generales, por ejemplo, un ´arbol AVL debe cumplir ciertas condiciones sobre las alturas de los hijos o un ´arbol rojinegro debe cumplir que las alturas negras de cada hijo sean iguales. Sin embargo, otros predicados son puramente estructurales, como es el caso de que un mont´ıculo sea zurdo. Para los primeros, las llamadas Miguel Garrido Canalejas 4.1. TIPOS DE RESTRICCIONES 47 a estas funciones nos verificar´an internamente que se cumpla la restricci´on estructural requerida, devolviendo unsat en caso de no hacerlo. Si lo verifica, proseguir´a con el resto de comprobaciones aunque podr´ıa fallar por otro lado por alguna otra restricci´on. Por su parte, para los segundos, la llamada comprobar´a exclusivamente la restricci´on estructural devolvi´endonos directamente si se cumple o no. Ilustramos estas ideas con dos ejemplos. Si yo pido a Z3 que verifique la siguiente restricci´on (assert (isAVL t)), con tun ´arbol AVL y la funci´on isAVL definida como en la Figura 3.44, comprobar´a aspectos sobre las alturas de los hijos, entre otras consideraciones. Sin embargo, si yo pido verificar una restricci´on como (assert (isLeftist t)), donde tes un ´arbol binario e isLeftist corresponde a la funci´on definida en la Figura 3.36, estamos tratando con una funci´on puramente estructural que solo hace comprobaciones sobre las alturas m´ınimas. Concluimos las restricciones de estructura con algunos casos particulares, que son la altura negra de los ´arboles rojinegros y la altura de los ´arboles AVL. Al tratarse de alturas, estamos evidentemente ante restricciones estructurales, con las mismas limitaciones que el resto, es decir, no podemos construir un ´arbol desde cero a partir de una serie de aspectos sobre la altura negra. De este modo, por ejemplo para la primera, tendremos que utilizarla para verificar si una estructura de ´arbol rojinegro tiene una altura negra u otra y ver si se adapta a lo necesitado. Sin embargo, la altura negra, entre otras cosas analiza los colores de los nodos. Tales colores, si recordamos, eran un campo m´as de un ´arbol rojinegro, al que esperamos darle un valor. Es decir, los colores son parte del contenido del ´arbol. Por ello,estas restricciones referidas a la altura negra, si bien no pueden construir un ´arbol, podr´an servirnos como restricciones de contenido, tal y como explicaremos a continuaci´on, para dar valores a los colores. Lo mismo ocurre entonces con el campo de altura almacenado en un ´arbol AVL y las restricciones sobre la altura de estos ´arboles. 4.1.3. Restricciones de contenido Trabajar´an sobre el contenido de nuestra estructura, es decir, sobre los datos que la compongan. Estas restricciones, al contrario que las anteriores, nos permiten los dos m´etodos de usos comentados en la Secci´on 3.7. Podemos, por un lado, comprobar si una variable con ciertos valores guardados cumple una restricci´on y, por otro lado, rellenar una estructura concreta. El enfoque verdaderamente interesante y novedoso es el segundo, y es el que aporta la potencia a este trabajo, pues nos servir´a para crear todos los valores sin necesidad de filtrarlos despu´es. Nos centraremos entonces en ´este, analizando como rellenar estructuras. Comentaremos primero los casos elementales de contenido, para luego analizar las particularidades introducidas en las restricciones estructurales. Trabajo Fin de Grado 48 CAP´ ITULO 4. ESTRATEGIA DE GENERACI´ ON DE CASOS (declare-const u (Arr Int)) (declare-const v (Arr Int)) (assert (= (second u) 4)) (assert (= (second v) 4)) (assert (permut u v)) Figura 4.1: Comprobaci´on de la permutaci´on de dos arrays (define-fun k!19 ((x!0 Int)) Int (ite (= x!0 2) 11 (ite (= x!0 3) 7 (ite (= x!0 1) 7 (ite (= x!0 0) 7 5))))) (define-fun k!20 ((x!0 Int)) Int (ite (= x!0 2) 7 (ite (= x!0 3) 7 (ite (= x!0 1) 11 (ite (= x!0 0) 7 6))))) Figura 4.2: Modelo obtenido tras ejecutar la funci´on permut Cuando hablamos de contenido, hablamos de los valores almacenados en arrays, listas o ´arboles. Distinguimos la forma de trabajar con arrays respecto a las otras dos. Y es que, al tener Z3 soporte para arrays, la forma de crear contenido puede hacerse de forma m´as directa que en los otros casos. Comentamos cada perspectiva. Al trabajar con arrays, Z3 nos proporciona una representaci´on interna en forma de funci´on. Las funciones sortedArr ypermut trabajan sobre el contenido de los arrays. Pues bien, simplemente llamando a la primera con un array de una longitud determinada, Z3 nos crear´a directamente los valores almacenados en cada posici´on del array verificando la propiedad de orden. Por su parte, para la segunda, si le pasamos dos arrays con una cierta longitud fijada para cada uno de ellos (misma longitud pues tiene que haber el mismo n´umero de elementos), de nuevo Z3 crea los dos arrays correctamente. Pero adem´as, no solo es capaz de crear ambos arrays de cero, sino que, en caso de que uno de los dos tenga ya valores y el otro no, puede rellenar las distintas posiciones del segundo con los elementos que conforman el primero, verificando que el array resultante sea permutaci´on del de partida. Vemos en la Figura 4.1 qu´e ocurre al llamar a la funci´on permutaci´on. Los dos arrays se crean vac´ıos, y ´unicamente se les asigna una longitud a cada uno de ellos. El modelo obtenido (Figura 4.2) verifica que el array u, definido como la funci´on k!19, tiene los mismos elementos que v, que corresponde a la funci´on k!20, aunque en distinto orden, es decir, efectivamente uno es permutaci´on del otro. Miguel Garrido Canalejas 4.2. ESTRATEGIA 49 Por su parte, al trabajar con listas o ´arboles la tarea se vuelve algo m´as compleja. Al contrario que para los arrays, la definici´on de estos tipos no es interna de Z3 sino que nos la hemos creado nosotros con nuestros tipos algebraicos correspondientes. Por ello, para trabajar con cualquier elemento de uno de estos tipos necesitamos tener especificada previamente una estructura concreta. Esta estructura vendr´a vac´ıa, es decir, con los nodos sin ning´un valor almacenado en ellos, sino con variables del tipo que corresponda seg´un el campo, que son las que esperamos que Z3 nos instancie con valores adecuados. Por tanto, al contrario que con los arrays, en los que nos bastaba definir la variable y darle una longitud, aqu´ı tendremos que darle a la variable concreta una cierta estructura. Comentamos, por ´ultimo, esa dualidad para algunas de las restricciones de estructura. Como hemos mencionado, aspectos como la altura de un AVL o la altura negra de un ´arbol rojinegro refieren a campos del propio tipo de datos. Por ello, podremos usarlas tambi´en para rellenar estos par´ametros. De este modo, si a una cierta estructura de ´arbol de tipo LLRB le pedimos que compruebe que sea efectivamente rojinegro, es decir, llamamos a la funci´on isLlrb de la Figura 3.55, entre las comprobaciones que realiza encontramos algunas que se refieren a los colores, y entre ellas la de las alturas negras de los hijos. As´ı, todas estas restricciones en conjunto nos devolver´ıan valores para cada uno de los colores de los nodos. En la Figura 4.3, vemos que aparece declarado un ´arbol rojinegro, adem´as de una serie de variables enteras y de color para construir la estructura del ´arbol. Pues bien, al pedir que compruebe la funci´on isLlrb, obtenemos el modelo de la Figura 4.4, en el que podemos ver que el ´arbol ha quedado completamente instanciado, con todas las variables de color tomando un valor concreto. En la Figura 4.5 podemos ver la representaci´on del modelo en forma de ´arbol, a fin de hacer m´as c´omoda la interpretaci´on de los valores obtenidos. El ´arbol obtenido es efectivamente un ´arbol rojinegro correcto. 4.2. Estrategia Hasta ahora hemos visto c´omo trabajar con cada tipo de restricci´on. A continuaci´on, veremos c´omo esta distinci´on nos facilitar´a la generaci´on de casos gracias a la estrategia seguida. Podemos distinguir cuatro etapas: fijar un tama˜no para los casos de prueba, generar estructuras de ese tama˜no, aplicar las restricciones de estructura correspondientes a las estructuras generadas y por ´ultimo popular tales estructuras. Con estas etapas lo que se pretende es salvar las limitaciones de Z3 a la hora de trabajar con las restricciones de tama˜no y estructura y aprovechar despu´es su potencia al tratar las de contenido. Como Z3 no es capaz de generar estructuras dado un cierto tama˜no, las dos primeras etapas se realizan desde Haskell. Despu´es, las estructuras creadas se pasan a Z3, donde se resuelven las siguientes dos etapas, consiguiendo poblar tales estructuras y obteniendo, con ello, nuestro caso de prueba final. Trabajo Fin de Grado 56 CAP´ ITULO 5. EXPERIMENTOS Funci´on Entrada Precondici´on Descripci´on InsertList x:Int, l :Lst {sortedList(l)}Inserta el elemento xordenadamente en l DeleteList x:Int, l :Lst {member(x, l)}Elimina el elemento xde la lista l Tabla 5.1: Funciones para listas cada caso los resultados obtenidos para diferentes tama˜nos de lista. Sorted Nuestra intenci´on aqu´ı es poblar diferentes estructuras de listas con una longitud dada, cumpliendo que la lista resultante est´e ordenada. Con el fin de aportar una cantidad de ejemplos suficientes, trabajaremos listas de cardinales desde dos hasta seis. Enumeramos a continuaci´on todos los resultados obtenidos para cada uno de esos tama˜nos: •(cons 0 (cons 1 nil)) •(cons (- 1) (cons 0 (cons 1 nil))) •(cons 0 (cons 1 (cons 2 (cons 3 nil)))) •(cons 0 (cons 1 (cons 2 (cons 3 (cons 4 nil))))) •(cons (- 1) (cons 0 (cons 1 (cons 2 (cons 3 (cons 4 nil)))))) Puede verse que en todos ellos, la lista generada est´a ordenada, de modo que Z3 est´a poblando correctamente nuestras estructuras de lista. Member Si en el caso anterior busc´abamos listas ordenadas, aqu´ı el orden de los elementos no nos interesa, lo ´unico importante es que el elemento xpertenezca a la lista. Por tanto, Z3 no solo tiene la tarea de generar la lista, sino que adem´as deber´a instanciar esa variable xcon un cierto valor y asegurar que ´este sea uno de los elementos que la conforman. De nuevo, estudiaremos las listas generadas seg´un los tama˜nos elegidos. Quedan enumeradas a continuaci´on todas estas listas junto al valor asignado a la variable x: Miguel Garrido Canalejas 5.2. ARRAYS 57 Funci´on Entrada Precondici´on Descripci´on InsertA x:Int, m : Int, a :Array {0≤m < length(a)∧ sortedArr(a, 0, m)} Inserta el elemento xen el array a Tabla 5.2: Funciones para arrays •x=0: (cons 0 (cons (- 2) nil)) •x=0: (cons 0 (cons (- 2) (cons 2 nil))) •x=0: (cons 0 (cons (- 2) (cons 2 (cons 3 nil)))) •x=0: (cons 0 (cons (- 2) (cons 2 (cons 3 (cons 3 nil))))) •x=0: (cons 0 (cons (- 2) (cons 2 (cons 3 (cons 3 (cons 4 nil)))))) En todos los casos encontramos que el valor asignado a xes cero, y que este valor se encuentra en todas las listas. Por ello, el modelo proporcionado por Z3 para cada tama˜no es tambi´en correcto en este caso. A fin de probar alg´un resultado diferente, a˜nadimos manualmente una restricci´on en la que forcemos a la xa tomar un valor diferente de cero o uno. El modelo que proporciona entonces Z3, para una lista de cinco elementos, es: •x=2: (cons 2 (cons 0 (cons (-2) (cons 2 (cons 3 nil))))) 5.2. Arrays El predicado m´as importante que nos encontramos para arrays es sortedArr, que comprueba si un cierto array est´a ordenado entre dos posiciones dadas. Para probar tal predicado, hemos usado la funci´on de inserci´on que aparece en la Tabla 5.2. Vemos que la funci´on recibe como par´ametro un array, el elemento a insertar en ´el y la posici´on en la que hacerlo (m). La precondici´on requiere que la posici´on en la que insertar est´e dentro de los l´ımites del array, y que ´este est´e ordenado entre el principio y dicha posici´on. De este modo, dado que la precondici´on afecta tanto al array como al par´ametro de entrada m, Z3 deber´a encontrar valores adecuados para ambos. Comentaremos algunos resultados obtenidos para diferentes longitudes del array de entrada. En primer lugar consideramos como longitud del array cuatro. El modelo devuelto por Z3 puede verse en la Figura 5.1. Vemos que el array viene definido a partir de la funci´on k!0. Esta funci´on devuelve: -2 si recibe un 0; 2 si recibe un 1; y 3 en cualquier otro caso. Adem´as, la variable mha tomado el valor cero. Esto quiere decir que el array debe estar ordenado entre las posiciones cero y cero, lo que es trivial y se cumple sea cual sea el valor que le haya dado al array, as´ı que, en particular, nuestros valores lo cumplen. Trabajo Fin de Grado 58 CAP´ ITULO 5. EXPERIMENTOS (define-fun a () (Pair (Array Int Int) Int) (mk-pair (_ as-array k!0) 4)) (define-fun m () Int 0) (define-fun k!0 ((x!0 Int)) Int (ite (= x!0 1) 2 (ite (= x!0 0) (- 2) 3))) Figura 5.1: Modelo para array de longitud cuatro (define-fun a () (Pair (Array Int Int) Int) (mk-pair (_ as-array k!0) 5)) (define-fun m () Int 0) (define-fun k!0 ((x!0 Int)) Int (ite (= x!0 1) 2 (ite (= x!0 0) (- 2) (ite (= x!0 4) 4 3))) Figura 5.2: Modelo para array de longitud cinco Vamos a considerar ahora que la longitud del array es cinco. En este caso, el modelo que nos proporciona Z3 es el de la Figura 5.2. De nuevo, la mtoma el valor cero, as´ı que razonando del mismo modo que hemos hecho antes, podemos afirmar que el array proporcionado por Z3 es correcto. Que Z3 instancie la msiempre a cero es un caso que repite cualquiera que sea la longitud que le pongamos al array. Estos casos, como ya hemos visto son triviales as´ı que vamos a forzar a buscar alg´un caso algo m´as complicado. Para ello, tomamos arrays de longitud seis y, a˜nadiremos manualmente dos restricciones con las que prohibir a Z3 que le de a la variable mlos valores cero o uno. Con todo esto, el modelo que nos proporciona el resolutor es el que aparece en la Figura 5.3. En este caso, Z3 ha elegido cinco como valor para la m. Por tanto, la precondici´on pide en este caso que el array completo est´e ordenado. Si nos fijamos en la funci´on k!0 que es la que define a nuestro array, vemos que devuelve -1 en caso de recibir como entrada un cero, un 3 en caso de recibir un 5, y un 0 en cualquier otro caso. Si representamos esta funci´on en forma de array como en la Figura 5.4, se ve f´acilmente que el array cumple que est´a ordenado. Miguel Garrido Canalejas 5.3. ´ ARBOLES BINARIOS 59 (define-fun a () (Pair (Array Int Int) Int) (mk-pair (_ as-array k!0) 6)) (define-fun m () Int 5) (define-fun k!0 ((x!0 Int)) Int (ite (= x!0 5) 3 (ite (= x!0 0) (- 1) 0))) Figura 5.3: Modelo para array de longitud seis con mdistinto de cero o uno Figura 5.4: Modelo de array de cardinal seis 5.3. ´ Arboles Binarios Los ´arboles binarios sirven para representar diferentes estructuras. De entre las m´as interesantes, las que decidimos tratar en el Cap´ıtulo 3 fueron los mont´ıculos, concretamente los zurdos, y los ´arboles de b´usqueda (BST). Por ello, las funciones estudiadas a lo largo de esta secci´on referir´an a ambos tipos. 5.3.1. Mont´ıculos Zurdos Dentro de los distintos tipos de mont´ıculos, uno de los m´as interesantes a probar son los zurdos, puesto que nos aportan una clara separaci´on entre propiedades estructurales, referidas a las alturas m´ınimas, y de contenido, sobre el orden de los elementos dentro del ´arbol. De este modo, los predicados m´as importantes a la hora de trabajar con estos mont´ıculos son isLeftist, encargado de comprobar si la estructura es adecuada, e isHeap, que har´a lo propio con el contenido. Por tanto, las funciones que vamos a analizar incluyen en sus precondiciones tales predicados, como puede verse en la Tabla 5.3. Dado que los predicados de ambas precondiciones son los mismos, utilizaremos la primera para analizar los resultados obtenidos para diferentes cardinales, y despu´es mostraremos algunos de los modelos proporcionados para la segunda, a fin de ver el comportamiento de Z3 al trabajar con dos estructuras a la vez. As´ı, para la primera funci´on comentaremos primero los modelos para cardinales dos y tres, analizaremos algunos de cardinales superiores y veremos al final una estad´ıstica de casos aceptados y rechazados. Por su parte, para la segunda, aplicaremos a las dos estructuras que participan los distintos razonamientos expuestos para la anterior funci´on, viendo algunos resultados para cardinales diferentes. Trabajo Fin de Grado 60 CAP´ ITULO 5. EXPERIMENTOS Funci´on Entrada Precondici´on Descripci´on InsertLeft x:Int, t :T ree {isLeftist(t)∧ isHeap(t)} Inserta xen el mont´ıculo t UnionLeft t1 : Tree, t2 : T ree {(isLeftist(t1)∧ isHeap(t1)) ∧ (isLeftist(t2) ∧ isHeap(t2))} Une dos mont´ıculos zurdos Tabla 5.3: Funciones para mont´ıculos zurdos (a) (b) Figura 5.5: Estructuras de un ´arbol binario de dos nodos Antes de entrar a comentar los resultados, conviene recordar las dos restricciones que deben cumplirse. En primer lugar, debe ocurrir que la altura m´ınima del hijo izquierdo debe ser mayor o igual que la del hijo derecho y, en segundo lugar, el valor almacenado en la ra´ız debe ser menor o igual que el de sus hijos. Cuando trabajamos con ´arboles de cardinal dos, ´unicamente podemos encontrarnos dos estructuras diferentes, que aparecen en la Figura 5.5. Resulta sencillo ver que la primera de las estructuras s´ı que cumple la restricci´on estructural requerida, puesto que la altura m´ınima del hijo izquierdo es uno mientras que la del derecho es cero, pero que, por el contrario, la segunda la incumple ya que la altura m´ınima del hijo derecho es uno, que es mayor que la del hijo izquierdo que es cero. Como era de esperar, al ejecutar nuestras restricciones en Z3 obtenemos que efectivamente el caso correspondiente a la segunda estructura es insatisfactible. Por su parte, para el primero obtenemos el modelo (node 0 (node 3 leaf leaf) leaf), que cumple que la ra´ız es menor que el hijo izquierdo, como dese´abamos. Puede verse la representaci´on del modelo obtenido en forma de ´arbol en la Figura 5.6. Al trabajar con cardinal tres, el n´umero de estructuras posibles crece a cinco, representadas todas ellas en la Figura 5.7. Dado que la condici´on estructural que tiene que cumplirse requiere que la altura m´ınima del hijo izquierdo sea mayor o igual que la del derecho, vemos r´apidamente que las estructuras de las Figuras 5.7d y 5.7e no podr´an satisfacer nuestra precondici´on. Pero adem´as, la propiedad para ser zurdo era recursiva, de modo que los hijos tambi´en deben cumplirla. Si nos fijamos en la estructura de la Figura 5.7b, vemos que para el hijo izquierdo, sus respectivos hijos incumplen la propiedad sobre las alturas m´ınimas. Pues bien, al pasar nuestro fichero de restricciones por Z3, obtenemos unsat como resultado para estas tres estructuras y sat para el resto. As´ı, para estas estructuras satisfactibles obtenemos Miguel Garrido Canalejas 5.3. ´ ARBOLES BINARIOS 61 Figura 5.6: Modelo para mont´ıculo zurdo de cardinal dos adem´as los modelos (node (-3) (node (-3) (node 0 leaf leaf) leaf) leaf) para la Figura 5.7a y (node 0 (node 2 leaf leaf) (node 4 leaf leaf)) para la Figura 5.7c. Ambos modelos obtenidos aparecen reflejados en la Figura 5.8 A partir de aqu´ı veremos solo algunos ejemplos interesantes de modelos obtenidos para cardinales superiores. En la Figura 5.9a se muestra un modelo devuelto por Z3 para una estructura de cardinal cuatro. En primer lugar, verifica evidentemente la propiedad estructural, puesto que si no fuera as´ı no habr´ıa podido resolverla. Es una estructura interesante puesto que, al tener dos nodos en el hijo derecho y solo uno en el izquierdo podr´ıa llevarnos a enga˜no. Sin embargo, la altura m´ınima del hijo derecho es uno, igual que la del izquierdo. En segundo lugar, vemos que los valores asignados a cada nodo cumplen ser menores o iguales que los de sus respectivos hijos. Con todo ello, el modelo obtenido es correcto. Por su parte, en las Figuras 5.9b y 5.9c aparecen dos nuevos modelos, uno de cardinal cinco y otro de cardinal seis. De nuevo, si nos fijamos en los valores proporcionados por Z3 para rellenar cada uno de los nodos, vemos que ambos modelos vuelven a ser correctos puesto que respetan el orden requerido, al cumplirse siempre que la ra´ız es menor o igual que sus hijos. Para la segunda funci´on, la ´unica diferencia es que en vez de trabajar sobre una ´unica estructura lo haremos sobre dos, y en consecuencia, la precondici´on afecta a ambas, comprobando que sean mont´ıculos zurdos. As´ı, las condiciones a cumplir son exactamente las mismas, por lo que los razonamientos a la hora de identificar estructuras v´alidas son totalmente an´alogos a los realizados hasta ahora con la primera funci´on. De este modo, si por ejemplo, tenemos un caso en el que se combinan las estructuras de las Figuras 5.7c y 5.5b, la primera cumplir´ıa las restricciones pero la segunda no, de manera que la restricci´on derivada de la precondici´on ser´ıa insatisfactible. Por el contrario, si por ejemplo se han combinado las estructuras de las Figuras 5.7a y 5.7c, al ser ambas v´alidas, como ya vimos previamente, la restricci´on en este caso s´ı ser´ıa satisfactible, y Z3 devolver´ıa los modelos apropiados. A fin de mostrar un ejemplo con el que ilustrar que efectivamente rellena correctamente dos estructuras, en la Figura 5.10 puede verse el modelo obtenido para dos ´arboles, el primero de cardinal tres y el segundo de cardinal cuatro, ambos correctos tanto estructuralmente como en lo que refiere al orden de sus elementos. Por ´ultimo, en la Tabla 5.4 se muestran el n´umero de casos satisfactibles e insatisfactibles obtenidos para cardinales cuatro, cinco y seis. Trabajo Fin de Grado 62 CAP´ ITULO 5. EXPERIMENTOS (a) (b) (c) (d) (e) Figura 5.7: Estructuras de un ´arbol binario de tres nodos 5.3.2. ´ Arboles de B´usqueda Las funciones utilizadas para probar los ´arboles de b´usqueda aparecen descritas en la Tabla 5.5. Todas ellas reciben como par´ametro de entrada una variable t de tipo Tree, y comparten como precondici´on la llamada al predicado isBST, encargado de comprobar si un cierto ´arbol es o no de b´usqueda. Para analizar los resultados obtenidos, mostraremos los modelos obtenidos para estructuras de cardinal dos y tres, luego comentaremos algunos modelos interesantes de tama˜no cuatro o cinco. Si recordamos la funci´on isBST de Z3, expuesta en el Cap´ıtulo 3, no presentaba ninguna restricci´on de car´acter estructural, y ´unicamente se limitaba a comprobar que los elementos estuvieran ordenados de manera adecuada. Por ello, para todas las estructuras obtendremos que la restricci´on isBST es satisfactible, junto a un modelo adecuado para cada una de ellas. Por tanto, no entraremos a analizar la posible satisfactibilidad de las diferentes estructuras, puesto que todas van a serlo, sino que ´unicamente estudiaremos los resultados obtenidos a fin de ver si cumplen lo esperado. Para ´arboles binarios de cardinal dos, encontramos ´unicamente dos posibles estructuras. Al ejecutar Z3, los modelos obtenidos son (node 1 (node 0 leaf leaf) leaf) para la estructura de la Figura 5.5a y (node (- 1) leaf (node 0 leaf leaf)) para la estructura de la Figura 5.5b. En ambos casos, los valores asigMiguel Garrido Canalejas 5.3. ´ ARBOLES BINARIOS 63 (a) (b) Figura 5.8: Mont´ıculos zurdos de tres nodos Cardinal Casos Satisfactibles Casos Insatisfactibles Cuatro 4 10 Cinco 8 34 Seis 17 115 Tabla 5.4: Resultados obtenidos para mont´ıculos zurdos nados a los nodos son correctos puesto que, en el primero, la ra´ız es mayor que el hijo izquierdo, y en el segundo, la ra´ız es menor que el hijo derecho. Tales modelos pueden verse representados en forma de ´arbol en la Figura 5.11. Cuando el cardinal es tres, pasamos de tener dos posibles estructuras a cinco (Figura 5.7), todas ellas satisfactibles como coment´abamos previamente. As´ı, el resultado de ejecutar Z3 sobre nuestras restricciones, son cinco modelos diferentes para las cinco estructuras. Estos modelos quedan reflejados en la Figura 5.12, en la que podemos ver todas las estructuras de cardinal tres pobladas con diferentes valores. Vemos que en cada una de ellas, si descendemos por los diferentes sub´arboles, siempre se cumple que el hijo izquierdo sea menor que la ra´ız, y ´esta a su vez sea menor que el hijo derecho. Por tanto, todos los modelos proporcionados por Z3 son correctos. A partir de aqu´ı, el n´umero de estructuras generadas crece notablemente, por lo que solo mostraremos algunos ejemplos de cardinales cuatro y cinco con los que terminar de confirmar que Z3 est´a poblando correctamente nuestros ´arboles. En la Figura 5.13 encontramos tres posibles modelos para cardinal cuatro, mientras que en la Figura 5.14 aparecen dos alternativas para cardinal cinco. En todas ellas, de nuevo, se verifica que el orden de los elementos es correcto. Trabajo Fin de Grado 64 CAP´ ITULO 5. EXPERIMENTOS (a) Cardinal cuatro (b) Cardinal cinco (c) Cardinal seis Figura 5.9: Mont´ıculos zurdos de cardinales cuatro, cinco y seis 5.4. ´ Arboles AVL Para probar los ´arboles AVL hemos utilizado las funciones de inserci´on de un elemento, b´usqueda de un elemento, y borrado de un elemento. En la Tabla 5.6 quedan recogidas todas estas funciones con sus respectivas precondiciones, junto a algunos datos adicionales. Puede verse que en todas ellas se recibe como entrada de la funci´on un ´arbol de tipo AVL, sobre el que act´uan todas las precondiciones requiriendo que sea, efectivamente, un AVL. Dado que todas las precondiciones son entonces iguales, no separaremos por casos sino que analizaremos todas por igual, comentando los resultados obtenidos para diferentes tama˜nos de entrada. Comenzaremos analizando los resultados para tama˜nos dos y tres, comentaremos algunos casos representativos para tama˜nos mayores y, por ´ultimo, para tama˜nos mayores analizaremos el n´umero de estructuras rechazadas y aceptadas, a fin de saber cuantas se pueden poblar de todas las que se generan. Los ´arboles AVL contaban con un campo adicional para almacenar la altura de cada nodo, por lo que, para ver que el ´arbol creado por Z3 es correcto, tendremos que fijarnos tanto en el orden de los elementos como en este dato. Adem´as, conviene recordar que la propiedad estructural que debe cumplir un ´arbol para ser AVL es Miguel Garrido Canalejas 5.4. ´ ARBOLES AVL 65 (a) (b) Figura 5.10: Mont´ıculos zurdos de cardinales tres y cuatro para la funci´on de uni´on Funci´on Entrada Precondici´on Descripci´on InsertBST x:Int, t :T ree {isBST (t)}Inserta el elemento xen el ´arbol t SearchBST x:Int, t :Tree {isBST (t)}Busca el elemento xen el ´arbol t DeleteBST x:Int, t :T ree {isBST (t)}Elimina el elemento xdel ´arbol t Tabla 5.5: Funciones para ´arboles binarios de b´usqueda que la diferencia entre las alturas de los hijos no sea mayor que uno. A lo largo de la secci´on, cuando comentemos los casos descartados nos referiremos a esta propiedad. Si tenemos ´arboles binarios de cardinal dos, ´unicamente podemos encontrarnos dos estructuras, una con la ra´ız y un nodo en el hijo izquierdo, y la otra con la ra´ız y un nodo en el derecho. Ambas estructuras verifican ser AVL, puesto que en los dos casos la diferencia de alturas de los hijos no es mayor que uno. Por ello, cabr´ıa esperar que, al pedir a Z3 que resuelva nuestras restricciones, obtuvi´eramos que todos los casos son satisfactibles, y nos proporcionara, por tanto, un modelo para nuestras estructuras verificando tales restricciones. En efecto, Z3 resuelve los dos casos como sat y devuelve el modelo (nodeA 3 2 (nodeA 0 1 leafA leafA) leafA) para el ´arbol con hijo derecho vac´ıo (Figura 5.5a), y (nodeA (- 1) 2 leafA (nodeA 0 1 leafA leafA)) para el de hijo izquierdo vac´ıo (Figura 5.5b). En ambos casos, en cada nodo, el campo reservado para la altura toma los valores esperados (dos para la ra´ız y uno para el hijo), mientras que los valores almacenados respetan el orden requerido para ser ´arbol de b´usqueda, puesto que, en el primer caso, la ra´ız es mayor que el hijo izquierdo, y en el segundo, la ra´ız es menor que el hijo derecho. En la Figura 5.15 se muestran ambos modelos en forma de ´arbol. Con los ´arboles de cardinal tres empiezan a crecer el n´umero de estructuras generadas, recogidas todas ellas en la Figura 5.7. De entre las cinco posibles estructuras, ´unicamente aquella con un nodo como hijo izquierdo y otro como hijo Trabajo Fin de Grado 72 CAP´ ITULO 5. EXPERIMENTOS Funci´on Entrada Precondici´on Descripci´on InsertLLRB x:Int, t :LLRB {isLLRB(t)}Inserta el elemento xen el ´arbol t SearchLLRB x:Int, t :LLRB {isLLRB(t)}Busca el elemento xen el ´arbol t DeleteLLRB¨ Ix:Int, t :LLRB {isLLRB(t)}Elimina el elemento xdel ´arbol t Tabla 5.8: Funciones para ´arboles rojinegros Figura 5.19: Modelo para un ´arbol de dos nodos cenados en el sub´arbol izquierdo, y menor que aquellos almacenados en el derecho, cumpliendo as´ı que sea BST. Por otro lado, respecto a los colores, respetan que las alturas negras son iguales para cualquier camino desde la ra´ız a un nodo vac´ıo y, adem´as, el ´unico nodo rojo que nos aparece est´a a la izquierda. Por todo ello, el modelo proporcionado es totalmente correcto. Por otro lado, un posible modelo para ´arboles de cardinal cinco es el reflejado en la Figura 5.21b. En ´el vemos que por cualquier camino que elijamos la altura negra es siempre dos, por lo que se respeta la primera de las condiciones para que est´e correctamente coloreado. Adem´as, los dos nodos rojos que nos encontramos no est´an consecutivos y, aunque hay uno rojo como hijo derecho de un nodo, el correspondiente hijo izquierdo es tambi´en rojo. Por todo ello, los colores proporcionados por Z3 son correctos. Respecto a los valores que encontramos, tambi´en respetan el orden requerido, por lo que, en conjunto, todo el modelo vuelve a ser correcto. Por ´ultimo, para cardinal seis comenzamos a obtener modelos m´as interesantes con los que mostrar la potencia de Z3, pues empieza a tener que alternar colores en los diferentes caminos. Uno de los modelos obtenidos es el de la Figura 5.21c. En ´el podemos ver como, a lo largo del hijo izquierdo, va alternando nodos de color negro y rojo, a fin de conseguir respetar todas las condiciones requeridas. Vemos que la primera de ellas, referida a las alturas negras de los hijos, se cumple, puesto que por todos los posibles caminos desde la ra´ız a un nodo vac´ıo encontramos la misma altura negra. Por su parte, las referidas a los nodos rojos tambi´en se cumplen, puesto que no encontramos ni dos nodos rojos seguidos ni un nodo rojo como hijo derecho siendo el hijo izquierdo negro. Por tanto, todos los requisitos sobre el coloreado del ´arbol se satisfacen. Por su parte, en lo que refiere al orden de los Miguel Garrido Canalejas 5.5. ´ ARBOLES ROJINEGROS 73 Figura 5.20: Modelo para un ´arbol de cardinal 3 Cardinal Casos Satisfactibles Casos Insatisfactibles Cuatro 2 12 Cinco 3 39 Seis 4 128 Tabla 5.9: Resultados obtenidos para ´arboles LLRB valores almacenados, tambi´en se cumple la condici´on impuesta para ser BST. Con todo ello, el modelo analizado es correcto. Para concluir, en la Tabla 5.9 quedan recogidos los datos sobre el n´umero de casos satisfactibles e insatisfactibles seg´un el cardinal del ´arbol. Podemos ver que son muy pocas las estructuras que Z3 puede rellenar, puesto que la mayor´ıa de los casos son insatisfactibles. Si bien de primeras puede resultar chocante que sean tantas las estructuras descartadas, todas las restricciones de color son, en conjunto, tan restrictivas, que esto puede ocurrir. Y es que, en primer lugar, en todas aquellas estructuras en las que no haya un cierto equilibrio entre los nodos que encontramos a la izquierda y la derecha de la ra´ız, resultar´a imposible conseguir que las alturas negras sean iguales. Descartadas todas estas, a´un teniendo ese cierto equilibrio, hay muchas en las que el hijo izquierdo de un nodo es vac´ıo mientras que el derecho no lo es, y a ´este le corresponder´ıa el color rojo, situaci´on prohibida tambi´en. En conclusi´on, resulta muy complicado verificar todas las restricciones involucradas en el predicado isLLRB, haciendo as´ı que muchas de las estructuras generadas sean descartadas. Viendo que son tantas las estructuras rechazadas, podr´ıa pensarse que nuestro sistema no est´a aportando ninguna mejor´ıa. Si consideramos la generaci´on de casos de prueba anterior, en la que se generaba aleatoriamente la estructura, la probabilidad de que fuera mala, y por tanto descartada, era igual que en nuestro caso, puesto que las comprobaciones a realizar son exactamente las mismas. Sin embargo, adem´as de generarse aleatoriamente la estructura, se generaban tambi´en los valores almacenados en ella y los colores de cada nodo. Estos valores deb´ıan pasar el correspondiente filtro, haciendo que, aunque la estructura fuera correcta, hubiera que descartarla por incumplir tales valores alguna propiedad. Esto en cambio no ocurre en nuestro sistema, puesto que una vez tenemos las estructuras buenas, es imposible que los valores que las rellenen sean incorrectos. Trabajo Fin de Grado 74 CAP´ ITULO 5. EXPERIMENTOS (a) Cardinal 4 (b) Cardinal 5 (c) Cardinal 6 Figura 5.21: Modelos para cardinales cuatro, cinco y seis Para concluir la secci´on, vamos a analizar, en t´erminos de eficiencia, el comportamiento de nuestro sistema. Lo hacemos para ´arboles rojinegros ya que son los que tienen que hacer mayor n´umero de comprobaciones y generar los modelos m´as complejos, siendo por tanto en los que peores resultados pueden obtenerse. En primer lugar, mencionar que al proporcionarnos Z3 un modelo, ´esto no solo consiste en dar valor a las variables sino que todas las funciones declaradas forman parte del modelo. Por tanto, parte del tiempo lo ocupa en escribir todas estas funciones para cada modelo y, del mismo modo, la mayor parte de las l´ıneas del fichero de salida se corresponden con todas ellas. Por ello, los resultados mostrados a continuaci´on son, primero contando con la escritura de todas estas funciones para cada modelo, y despu´es teniendo solo en cuenta la resoluci´on de la satisfactibilidad de cada posible estructura. En la Tabla 5.10 se muestran los tiempos de ejecuci´on para generar todos los modelos de diferentes cardinales, primero teniendo que escribir todo el modelo y despu´es teniendo en cuenta solo la resoluci´on de la satisfactibilidad de cada caso. Vemos que hasta cardinal seis los tiempos son bastante bajos, pero a partir de cardinal ocho se disparan. Esto parece l´ogico pues tenemos hasta 1430 estructuras Miguel Garrido Canalejas 5.5. ´ ARBOLES ROJINEGROS 75 Cardinal Tiempo modelo completo Tiempo satisfactibilidad Tres 0.134s0.128s Cuatro 0.222s0.163s Cinco 0.481s0.369s Seis 1.149s1.018s Ocho 12.075s11.645s Tabla 5.10: Tiempos de ejecuci´on diferentes. Otro aspecto que se observa es que difieren poco los tiempos con modelo de los de sin modelo. El n´umero de estructuras rechazadas para estos ´arboles era muy elevado, por lo que son pocos los modelos que tiene que escribir en el primero de los casos. Por ´ultimo, respecto al n´umero de l´ıneas del fichero final de salida, mostramos solo alg´un dato con el que hacernos a la idea de lo que ocupa cada cosa. Si tomamos por ejemplo estructuras de cardinal cinco, el fichero obtenido consta de 871 l´ıneas. Sin embargo, si cogemos uno de los modelos proporcionados, resulta que solo 25 son de las variables que nos interesan, mientras que 240 son del resto de funciones. Por tanto, ser´a principalmente esto ´ultimo lo que haga que el n´umero de l´ıneas se eleve cuando tengamos m´as casos satisfactibles y, por tanto, m´as modelos. Trabajo Fin de Grado 76 CAP´ ITULO 5. EXPERIMENTOS Miguel Garrido Canalejas Cap´ıtulo 6 Conclusiones Castellano Llegados hasta este punto, podemos afirmar que los objetivos que se marcaron al comienzo del trabajo han sido cumplidos. Como primer gran objetivo, nos planteamos ser capaces de transformar un aserto-precondici´on en un conjunto de restricciones. Gracias al programa Haskell creado, expuesto en el Ap´endice A, podemos transformar la precondici´on de una funci´on, dada en su representaci´on intermedia, en una serie de restricciones procesables por Z3 con las que generar autom´aticamente casos de prueba a partir de su satisfactibilidad Por otro lado, se plante´o como segundo reto la investigaci´on de los resolutores SMT, concretamente de Z3, con la intenci´on de codificar en esta plataforma todos los posibles predicados involucrados en las distintas precondiciones de algunas de las funciones m´as interesantes sobre las estructuras de datos tratadas. Durante el Cap´ıtulo 3, abordamos la explicaci´on de la transformaci´on de los diferentes asertos en funciones de Z3, mostrando adem´as la potencia de esta herramienta para dar valor a las diferentes variables involucradas en las restricciones planteadas. Los resultados desprendidos de esta investigaci´on fueron dispares. Y es que, si bien se ha descubierto que es muy potente a la hora de dar valor a variables de tipos sencillos como enteros o arrays, cuando tiene que sintetizar estructuras algebraicas como ´arboles o listas, es incapaz de hacerlo. Sin embargo, gracias a la estrategia planteada sobre separar las restricciones en diferentes tipos, hemos logrado salvar esta dificultad de Z3, consiguiendo que nuestro sistema sea bastante eficaz. Con todo esto, hemos logrado cumplir la tarea de generar casos de prueba que satisfagan una cierta precondici´on, partiendo ´unicamente de la especificaci´on de la misma. Respecto a las l´ıneas de trabajo a seguir en un futuro, la principal ampliaci´on del proyecto reside en hacer uso de la API de Z3 para Haskell. Mediante su utilizaci´on, ser´an dos las principales ventajas que se puedan obtener. En primer lugar, la automatizaci´on de todo el proceso de generaci´on de casos. Con nuestro tra77 78 CAP´ ITULO 6. CONCLUSIONES bajo, generamos un fichero smt a partir del cu´al, al ejecutarlo en Z3, obtenemos los diferentes casos de prueba buscados. Utilizando la API, podremos saltarnos el paso de crear dicho fichero obteniendo directamente los modelos que conforman los casos de prueba. En segundo lugar, la ventaja m´as importante es la posibilidad de generar un mayor n´umero de casos de prueba. Hasta ahora, con el fichero smt podemos dar un ´unico valor a cada una de nuestras estructuras. Gracias a la API de Z3, al poder tener acceso directo a los modelos proporcionados, podr´ıamos lograr este objetivo. Para ello, habr´ıa que analizar tales modelos para crear nuevas restricciones en las que ´estos sean negados, y volver a ejecutar despu´es consiguiendo entonces un modelo diferente al anterior. Iterando este proceso mientras queden combinaciones de valores a elegir, se podr´ıa entonces conseguir un mayor n´umero de casos de prueba para una misma estructura. Miguel Garrido Canalejas 79 Ingl´es At this stage, we can confirm that the stated goals at the beginning of this work have been accomplished. As the first main goal, we considered being able to transform a preconditionassertion into a set of restrictions. Thanks to the Haskell program we have created, displayed in the Appendix A, we can transform any function precondition, given in its intermediate representation, to a series of constraints processable by Z3, by which to automatically generate test cases from its satisfiability. On the other hand, the second challenge was the investigation of SMT solvers, Z3 in particular, with the intent of codifying in this platform all the predicates involved in the preconditions of some of the most interesting functions about the data structures we have considered. During Chapter 3, we explained the transformation of all the assertions into Z3 functions, showing, in addition, the power of this tool in giving values to the variables involved in the raised constraints. The results gathered from this investigation were disparate. On the one hand, while we have discovered Z3 is very powerful in giving values to simple type variables, such as integers or arrays, on the other hand it is unable to synthesize algebraic structures such as trees or lists. However, thanks to the proposed strategy of separating the constraints in different kinds, we have achieved to overcome this Z3 difficulty, so our system is quite effective. Following this, we have managed to complete the task of generating test cases satisfying a certain precondition, only from its specification. About the future work, the main extension of the project resides in using the Z3 API for Haskell. By using it, two advantages will be obtained. First, the automation of the entire case generation process. With our work, we generate a smt file from which, when executing it in Z3, we obtain the test cases we looked forward. Using the API, we may skip the step of creating such a file, directly obtaining the models which shape the test cases. Second, the most important advantage is the possibility of generating a larger number of test cases. Up to now, with the smt file we can give only one value to each of our structures. Thanks to the Z3 API, as we have direct access to the provided models, we could achieve this goal. In order to do that, those models should be analyzed in order to create new constraints which negate the model. Then, we will execute again the constraints obtaining a model different from the previous one. Iterating this process while it remains to exist combinations of the values, a larger number of test cases could be generated. Trabajo Fin de Grado 80 CAP´ ITULO 6. CONCLUSIONES Miguel Garrido Canalejas Ap´endice A Programa Haskell A lo largo de este ap´endice se muestra el c´odigo Haskell implementado encargado de traducir los archivos CLIR en ficheros smt. La funci´on principal se encuentra en un m´odulo Main, que hace uso de una serie de funciones definidas en el m´odulo Ast2Smt. El m´odulo principal se encarga de comprobar que los tipos de las variables son correctos, lee los datos de las funciones y las declaraciones de tipos creados en Z3, y escribe el fichero de salida. El m´odulo secundario es el encargado de transformar el ´arbol abstracto de la funci´on dada en una secuencia de cadenas en las que se declaren todas las variables necesarias y los asertos derivados de la precondici´on de dicha funci´on. Adem´as, este m´odulo es el encargado de generar las distintas estructuras para ciertos tipos de datos. Dado que todo el trabajo se engloba dentro un proyecto m´as grande, el c´odigo que se muestra a continuaci´on queda incluido dentro del proyecto Haskell ir2Haskell. Por ello, algunas de las llamadas a funciones que pueden encontrarse, o alguno de los m´odulos importados, no son propios de este trabajo sino que corresponden a trabajos previos sobre el proyecto global. A.1. Main module Main where import Ir2Haskell (parseAST, haskellcode) import Ast2Smt (filterVarsList, analyzeVars, allVars2String, paramsCases2String, obtainCasesList, getAssertion, casesList2String) import qualified Text.PrettyPrint.Mainland as D import Language.Clir import Data.List import qualified Data.Text as T ------------------------------------------------- --TIPOS CORRECTOS (ESTRUCTURAS ALMACENAN INT) ------------------------------------------------- 81 88 AP´ ENDICE A. PROGRAMA HASKELL analyzeType:: ClirType -> String analyzeType x = case x of SimpleType n -> T.unpack n TypeVar n -> T.unpack n CompoundType xs -> analyzeTypeList xs filterVarsList:: [(String, String)] -> [(String, String)] filterVarsList xs = [(x,y) | (x,y)<-xs, (not (elem y ["Int", "Bool"]))] ------------------------------------------------- --GENERADOR DE CASOS ------------------------------------------------- generateCases:: [(String, String)] -> [Int] -> [[String]] generateCases [x] [y] = case (snd x) of "Array" -> [] "Tree" -> [loadTrees (fst x) y] "Lst" -> [loadList (fst x) y] "LLRB" -> [loadLLRBs (fst x) y] "AVL" -> [loadAVLs (fst x) y] generateCases (x:xs) (y:ys) = case (snd x) of "Array" -> generateCases xs ys "Tree" -> (loadTrees (fst x) y):(generateCases xs ys) "Lst" -> (loadList (fst x) y):(generateCases xs ys) "LLRB" -> (loadLLRBs (fst x) y):(generateCases xs ys) "AVL" -> (loadAVLs (fst x) y):(generateCases xs ys) combineLists:: [[a]] -> [[a]] combineLists [] = [[]] combineLists (x:xs) = [x:y | x<-x, y<-(combineLists xs)] splits:: [a] -> [([a], [a])] splits xs = L.zip (L.inits xs) (L.tails xs) ---------------GENERADOR DE LISTAS--------------- loadList:: String -> Int -> [String] loadList x s = lists2String (generateList s x) lists2String:: [Lst] -> [String] lists2String [] = [] lists2String (x:xs) = oneList2String x:lists2String xs oneList2String:: Lst -> String oneList2String x = case x of Nil -> "nil" Cons c l -> "(cons " ++ c ++ " " ++ oneList2String l ++ ")" Miguel Garrido Canalejas A.2. AST2SMT 89 generateListAux:: String -> [Char] -> Lst generateListAux _ [] = Nil generateListAux n (x:xs) = Cons (n ++ [x]) (generateListAux n xs) generateList:: Int -> String -> [Lst] generateList n x = [generateListAux x (L.take n [’1’..])] --------------GENERADOR DE ´ ARBOLES--------------- loadTrees:: String -> Int -> [String] loadTrees x s = trees2String (generateTree s x) trees2String:: [Tree] -> [String] trees2String [] = [] trees2String (x:xs) = oneTree2String x:trees2String xs oneTree2String:: Tree -> String oneTree2String x = case x of Leaf -> "leaf" Node c l r -> "(node " ++ c ++ " " ++ oneTree2String l ++ " " ++ oneTree2String r ++ ")" generateTreeAux :: String -> [Char] -> [Tree] generateTreeAux _ [] = return Leaf generateTreeAux n (x:xs) = do (left, right) <- splits xs Node <$> pure (n++[x]) <*> generateTreeAux n left <*> generateTreeAux n right generateTree:: Int -> String -> [Tree] generateTree n x = generateTreeAux x (L.take n [’1’..]) ----------------GENERADOR DE AVL----------------- loadAVLs:: String -> Int -> [String] loadAVLs x s = avls2String (generateAVL s x) avls2String:: [AVL] -> [String] avls2String [] = [] avls2String (x:xs) = oneAvl2String x:avls2String xs oneAvl2String:: AVL -> String oneAvl2String x = case x of LeafA -> "leafA" NodeAvhlr->"(nodeA"++v++""++h++""++ oneAvl2String l ++ " " ++ oneAvl2String r ++ ")" Trabajo Fin de Grado 90 AP´ ENDICE A. PROGRAMA HASKELL generateAVLAux :: String -> [Char] -> [AVL] generateAVLAux _ [] = return LeafA generateAVLAux n (x:xs) = do (left, right) <- splits xs NodeA <$> pure (n++[x]) <*> pure (n++"h"++[x]) <*> generateAVLAux n left <*> generateAVLAux n right generateAVL:: Int -> String -> [AVL] generateAVL n x = generateAVLAux x (L.take n [’1’..]) ---------------GENERADOR DE LLRB----------------- loadLLRBs:: String -> Int -> [String] loadLLRBs x s = llrbs2String (generateLLRB s x) llrbs2String:: [LLRB] -> [String] llrbs2String [] = [] llrbs2String (x:xs) = oneLlrb2String x:llrbs2String xs oneLlrb2String:: LLRB -> String oneLlrb2String x = case x of LeafL -> "leafL" NodeLvclr->"(nodeL"++v++""++c++""++ oneLlrb2String l ++ " " ++ oneLlrb2String r ++ ")" generateLLRBAux :: String -> [Char] -> [LLRB] generateLLRBAux _ [] = return LeafL generateLLRBAux n (x:xs) = do (left, right) <- splits xs NodeL <$> pure (n++[x]) <*> pure (n++"c"++[x]) <*> generateLLRBAux n left <*> generateLLRBAux n right generateLLRB:: Int -> String -> [LLRB] generateLLRB n x = generateLLRBAux x (L.take n [’1’..]) ------------------------------------------------- --PARSING DE LOS CASOS ------------------------------------------------- obtainCasesList:: TopLevelDef -> [Int] -> [[String]] obtainCasesList x sizes = combineLists (generateCases (filterVarsList (analyzeVars x)) sizes) Miguel Garrido Canalejas A.2. AST2SMT 91 casesList2String:: [Assertion] -> [[String]] -> [(String, String)] -> String casesList2String a [x] y = "(push)\n" ++ cases2String a x y casesList2String a (x:xs) y = "(push)\n" ++ cases2String a x y ++ casesList2String a xs y cases2String:: [Assertion] -> [String] -> [(String, String)] -> String cases2String a [] [] = "\n" ++ assList2String a ++ "(pop)\n\n" cases2String a [] [(_, "Array")] = "\n" ++ assList2String a ++ "(pop)\n\n" cases2String a (x:xs) (y:ys) | (snd y) == "Array" = "" ++ cases2String a (x:xs) ys | otherwise = "(assert (= " ++ fst y ++ " " ++ x ++ "))\n" ++ cases2String a xs ys ------------------------------------------------- --PARSING DE LOS PAR´ AMETROS DE LOS CASOS ------------------------------------------------- paramsCases2String:: [(String, String)] -> [Int] -> String paramsCases2String [x] [y] = case (snd x) of "Array" -> sizeArr2String (fst x) y ++ paramsArr2String (fst x) (L.take y [’0’..]) "Lst" -> paramsList2String (fst x) (L.take y [’1’..]) "Tree" -> paramsTree2String (fst x) (L.take y [’1’..]) "LLRB" -> paramsLLRB2String (fst x) (L.take y [’1’..]) "AVL" -> paramsAVL2String (fst x) (L.take y [’1’..]) paramsCases2String (x:xs) (y:ys) = case (snd x) of "Array" -> sizeArr2String (fst x) y ++ paramsCases2String xs ys "Lst" -> paramsList2String (fst x) (L.take y [’1’..]) ++ paramsCases2String xs ys "Tree" -> paramsTree2String (fst x) (L.take y [’1’..]) ++ paramsCases2String xs ys "LLRB" -> paramsLLRB2String (fst x) (L.take y [’1’..]) ++ paramsCases2String xs ys "AVL" -> paramsAVL2String (fst x) (L.take y [’1’..]) ++ paramsCases2String xs ys sizeArr2String:: String -> Int -> String sizeArr2String n x = "(assert (= (second " ++ n ++ ") " ++ (show x) ++ "))\n\n" paramsArr2String:: String -> [Char] -> String paramsArr2String _ [] = "\n" paramsArr2String n (x:xs) = "(assert (> (select (first " ++ n ++ ") " ++ [x] ++ ") -5))\n" ++ "(assert (< (select (first " ++ n ++ ") " ++ [x] ++ ") 5))\n" ++ paramsArr2String n xs Trabajo Fin de Grado 92 AP´ ENDICE A. PROGRAMA HASKELL paramsList2String:: String -> [Char] -> String paramsList2String _ [] = "\n" paramsList2String n (x:xs) = "(declare-const " ++ n ++ [x] ++ " Int)\n" ++ "(assert (> " ++ n ++ [x] ++ " -5))\n" ++ "(assert (< " ++ n ++ [x] ++ " 5))\n" ++ paramsList2String n xs paramsTree2String:: String -> [Char] -> String paramsTree2String _ [] = "\n" paramsTree2String n (x:xs) = "(declare-const " ++ n ++ [x] ++ " Int)\n" ++ "(assert (> " ++ n ++ [x] ++ " -5))\n" ++ "(assert (< " ++ n ++ [x] ++ " 5))\n" ++ paramsTree2String n xs paramsLLRB2String:: String -> [Char] -> String paramsLLRB2String n xs = paramsLLRBVal2String n xs ++ paramsLLRBColor2String n xs paramsLLRBVal2String:: String -> [Char] -> String paramsLLRBVal2String n [x] = "(declare-const " ++ n ++ [x] ++ " Int)\n" ++ "(assert (> " ++ n ++ [x] ++ " -5))\n" ++ "(assert (< " ++ n ++ [x] ++ " 5))\n" paramsLLRBVal2String n (x:xs) = "(declare-const " ++ n ++ [x] ++ " Int)\n" ++ "(assert (> " ++ n ++ [x] ++ " -5))\n" ++ "(assert (< " ++ n ++ [x] ++ " 5))\n" ++ paramsLLRBVal2String n xs paramsLLRBColor2String:: String -> [Char] -> String paramsLLRBColor2String n [x] = "(declare-const " ++ n ++ "c" ++ [x] ++ " Color)\n" paramsLLRBColor2String n (x:xs) = "(declare-const " ++ n ++ "c" ++ [x] ++ " Color)\n" ++ paramsLLRBColor2String n xs paramsAVL2String:: String -> [Char] -> String paramsAVL2String n xs = paramsAVLVal2String n xs ++ paramsAVLHeight2String n xs paramsAVLVal2String:: String -> [Char] -> String paramsAVLVal2String n [x] = "(declare-const " ++ n ++ [x] ++ " Int)\n" ++ "(assert (> " ++ n ++ [x] ++ " -5))\n" ++ "(assert (< " ++ n ++ [x] ++ " 5))\n" paramsAVLVal2String n (x:xs) = "(declare-const " ++ n ++ [x] ++ " Int)\n" ++ "(assert (> " ++ n ++ [x] ++ " -5))\n" ++ "(assert (< " ++ n ++ [x] ++ " 5))\n" ++ paramsAVLVal2String n xs paramsAVLHeight2String:: String -> [Char] -> String paramsAVLHeight2String n [x] = "(declare-const " ++ n ++ "h" ++ [x] ++ " Int)\n" paramsAVLHeight2String n (x:xs) = "(declare-const " ++ n ++ "h" ++ [x] ++ " Int)\n" ++ paramsAVLHeight2String n xs Miguel Garrido Canalejas A.2. AST2SMT 93 ------------------------------------------------- --PARSING DE LAS VARIABLES ------------------------------------------------- allVars2String:: TopLevelDef -> String allVars2String (TopFunDef _ xs _ _ _) = varList2String xs varList2String:: [TypedVar] -> String varList2String [] = "\n" varList2String (x:xs) = var2String x ++ varList2String xs var2String:: TypedVar -> String var2String (TypedVar n x) = "(declare-const " ++ n ++ " " ++ type2String x ++ ")\n" typesList2String:: [ClirType] -> String typesList2String [] = "" typesList2String (x:xs) = type2String x ++ " " ++ typesList2String xs type2String:: ClirType -> String type2String (SimpleType n) | t =="Array" = "Arr" | otherwise = t where t= T.unpack n type2String (TypeVar n) = T.unpack n type2String (CompoundType xs) = "(" ++ typesList2String xs ++ ")" Trabajo Fin de Grado 94 AP´ ENDICE A. PROGRAMA HASKELL Miguel Garrido Canalejas Ap´endice B Resultados de Ejecuci´on Cuando ejecutamos nuestro programa Haskell sobre un fichero CLIR, obtenemos como salida un fichero smt con todas las restricciones necesarias, que es el que pasamos a Z3 para obtener as´ı los diferentes modelos. En este ap´endice se muestra tal fichero, a fin de poder comprobar que la traducci´on que realiza nuestro programa es correcta. La cabecera de este fichero es muy extensa y ´unicamente consta de las declaraciones de los tipos y las funciones de que se explicaron en el Cap´ıtulo 3. Por ello, aqu´ı lo ´unico que se muestra es la parte del fichero estrictamente perteneciente a la declaraci´on de variables y la creaci´on de restricciones a partir del fichero CLIR. El archivo mostrado corresponde a la traducci´on de la funci´on insertLLRB para ´arboles de cardinal tres. Adem´as, al ejecutar Z3 los modelos se vuelcan sobre un fichero txt desde el que poder analizar los resultados. Se muestra tambi´en en este ap´endice dicho fichero para la misma funci´on anterior. B.1. Fichero Smt (declare-const t (LLRB Int )) (declare-const x Int) (declare-const t1 Int) (assert (> t1 -5)) (assert (< t1 5)) (declare-const t2 Int) (assert (> t2 -5)) (assert (< t2 5)) (declare-const t3 Int) (assert (> t3 -5)) (assert (< t3 5)) (declare-const tc1 Color) (declare-const tc2 Color) (declare-const tc3 Color) 95 96 AP´ ENDICE B. RESULTADOS DE EJECUCI´ ON (push) (assert (= t (nodeL t1 tc1 leafL (nodeL t2 tc2 leafL (nodeL t3 tc3 leafL leafL))))) (assert (isLLRB t)) (check-sat) (get-model) (pop) (push) (assert (= t (nodeL t1 tc1 leafL (nodeL t2 tc2 (nodeL t3 tc3 leafL leafL) leafL)))) (assert (isLLRB t)) (check-sat) (get-model) (pop) (push) (assert (= t (nodeL t1 tc1 (nodeL t2 tc2 leafL leafL) (nodeL t3 tc3 leafL leafL)))) (assert (isLLRB t)) (check-sat) (get-model) (pop) (push) (assert (= t (nodeL t1 tc1 (nodeL t2 tc2 leafL (nodeL t3 tc3 leafL leafL)) leafL))) (assert (isLLRB t)) (check-sat) (get-model) (pop) (push) (assert (= t (nodeL t1 tc1 (nodeL t2 tc2 (nodeL t3 tc3 leafL leafL) leafL) leafL))) (assert (isLLRB t)) (check-sat) (get-model) (pop) Miguel Garrido Canalejas B.2. FICHERO TXT 97 B.2. Fichero Txt unsat (error "line 477 column 10: model is not available") unsat (error "line 486 column 10: model is not available") sat (model (define-fun tc1 () Color Negro) (define-fun t () (LLRB Int) (nodeL 1 Negro (nodeL 0 Negro leafL leafL) (nodeL 2 Negro leafL leafL))) (define-fun t3 () Int 2) (define-fun t2 () Int 0) (define-fun tc2 () Color Negro) (define-fun t1 () Int 1) (define-fun tc3 () Color Negro) (define-fun minTL ((x!0 (LLRB Int))) Int (ite (= x!0 leafL) 2000 (let ((a!1 (+ (minTL (izq x!0)) (* (- 1) (minTL (der x!0)))))) (let ((a!2 (ite (>= a!1 0) (minTL (der x!0)) (minTL (izq x!0))))) (ite (>= (+ (val x!0) (* (- 1) a!2)) 0) a!2 (val x!0)))))) (define-fun maxT ((x!0 (Tree Int))) Int (ite (= x!0 leaf) (- 2000) (let ((a!1 (+ (maxT (izq x!0)) (* (- 1) (maxT (der x!0)))))) (let ((a!2 (ite (<= a!1 0) (maxT (der x!0)) (maxT (izq x!0))))) (ite (<= (+ (value x!0) (* (- 1) a!2)) 0) a!2 (value x!0)))))) (define-fun multisetArr ((x!0 Int) (x!1 (Array Int Int)) (x!2 Int)) (Array Int Int) (ite (= x!0 x!2) ((as const (Array Int Int)) 0) ((_ map (+ (Int Int) Int)) (multisetArr (+ 1 x!0) x!1 x!2) (store ((as const (Array Int Int)) 0) (select x!1 x!0) 1)))) (define-fun cardA ((x!0 (AVL Int))) Int (ite (= x!0 leafA) 0 (+ 1 (cardA (izq x!0)) (cardA (der x!0))))) (define-fun k!0 ((x!0 Int)) Int 5) (define-fun k!29 ((x!0 (LLRB Int))) (LLRB Int) (ite (= x!0 (nodeL 0 Negro leafL leafL)) (nodeL 0 Negro leafL leafL) leafL)) (define-fun minHeight ((x!0 (Tree Int))) Int Trabajo Fin de Grado 104 BIBLIOGRAF´ IA Selected Papers, volume 9527 of Lecture Notes in Computer Science, pages 227– 243. Springer, 2015. Miguel Garrido Canalejas