Case Generator : implementación de una herramienta de pruebas basadas en asertos para una plataforma de verificación

Implementación de una herramienta de pruebas basadas en asertos para una plataforma de verificación Autor: Pedro García Castillo Director: Ricardo Peña Marí Facultad de Informática Universidad Complutense de Madrid Curso 2016-2017 13 de septiembre de 2017 2 ´ Indice 1 Resumen 5 1.1 Resumen................................... 5 1.2 Summary .................................. 6 1.3 Palabrasclave................................ 6 1.4 Keywords .................................. 6 2 Preliminares 7 2.1 ProyectoCAVI-ART............................ 7 2.2 QuickCheck................................. 8 2.2.1 Ejemplo de funcionamiento del programa . . . . . . . . . . . . 8 2.2.2 Leyes condicionales . . . . . . . . . . . . . . . . . . . . . . . . . 9 2.2.3 Monitorizando los datos . . . . . . . . . . . . . . . . . . . . . . 10 2.2.4 Como definir generadores . . . . . . . . . . . . . . . . . . . . . 10 2.3 Librer´ıa Generics de GHC . . . . . . . . . . . . . . . . . . . . . . . . . 11 2.4 TemplateHaskell.............................. 13 2.4.1 Un ejemplo de la idea b´asica . . . . . . . . . . . . . . . . . . . 13 2.4.2 Como usar template Haskell . . . . . . . . . . . . . . . . . . . . 13 2.4.3 Reification (Cosificaci´on) . . . . . . . . . . . . . . . . . . . . . 14 3 Nuestra propuesta: las clases Allv, Sized y Arbitrary 17 3.1 Black box testing en nuestro contexto . . . . . . . . . . . . . . . . . . 17 3.2 Sized..................................... 18 3.3 Allv/TemplateAllv............................. 19 3.4 Instancias predefinidas . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 4 El generador de casos 25 4.1 LainterfazconlaUUT .......................... 25 4.2 La obtenci´on del tipo de la UUT . . . . . . . . . . . . . . . . . . . . . 25 4.3 La generaci´on de instancias de Allv y Sized . . . . . . . . . . . . . . . 26 4.4 La generaci´on y ejecuci´on de casos . . . . . . . . . . . . . . . . . . . . 27 3 5 Experimentos 31 5.1 Insertar un elemento en una lista . . . . . . . . . . . . . . . . . . . . . 31 5.2 Insertar un elemento en un Array . . . . . . . . . . . . . . . . . . . . . 31 5.3 Insertar un elemento en un ´arbol . . . . . . . . . . . . . . . . . . . . . 32 5.4 B´usqueda en un ´arbol . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 5.5 Conclusiones de los experimentos . . . . . . . . . . . . . . . . . . . . . 33 6 Trabajo relacionado y conclusiones 35 6.1 Korat .................................... 35 6.2 Smallcheck ................................. 36 7 Conclusiones del proyecto 39 7.1 Conclusiones ................................ 39 7.2 Conclusions................................. 39 8 Ap´endice 41 8.1 Instancias predefinidas . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 8.2 Obtenci´on del tipo de la UUT . . . . . . . . . . . . . . . . . . . . . . . 42 8.3 Generaci´on de instancias de Allv . . . . . . . . . . . . . . . . . . . . . 44 8.4 Generaci´on y ejecuci´on de casos . . . . . . . . . . . . . . . . . . . . . . 47 8.5 UUTs de los diferentes casos de prueba . . . . . . . . . . . . . . . . . 48 8.5.1 Insertar en una lista ordenada . . . . . . . . . . . . . . . . . . . 48 8.5.2 Insertar en un Array . . . . . . . . . . . . . . . . . . . . . . . . 48 8.5.3 Insertar en un ´arbol . . . . . . . . . . . . . . . . . . . . . . . . 51 8.5.4 B´usqueda en un ´arbol . . . . . . . . . . . . . . . . . . . . . . . 52 4 Cap´ıtulo 1 Resumen 1.1 Resumen Una de las partes m´as costosas dentro del desarrollo de programas es el testeo, ya que requiere un gran esfuerzo humano para poder especificar los diferentes casos de prueba, lanzarlos y analizar los resultados. Ello provoca que en la mayor´ıa de los casos los programas se prueben mucho menos a fondo de lo que ser´ıa necesario. Por ello, en los ´ultimos a˜nos han sido desarrolladas diversas herramientas para automatizar de manera parcial dicho proceso de testeo. Sin embargo la mayor´ıa de ellas est´an especializadas en un ´unico lenguaje de programaci´on. Nuestro objetivo es conseguir una plataforma que permita el testeo de aplicaciones de manera autom´atica para el usuario y que admita como entrada un programa escrito en cualquier lenguaje de programaci´on. En este trabajo vamos a presentar la herramienta Case Generator, que se engloba dentro del proyecto CAVI-ART, siendo esta parte la encargada de generar los casos de prueba de manera automatizada, adapt´andolos a las necesidades de cada ejecuci´on. Este proyecto toma como base las ideas desarrolladas anteriormente por programas como Quickcheck, Korat o Smallcheck, pero intentando conseguir que el proceso de prueba sea m´as autom´atico, y a la vez compatible con diversos lenguajes de programaci´on tanto funcionales como no funcionales. Para lograr el primer objetivo hemos eliminado la obligaci´on de que el usuario defina un nuevo generador para cada uno de los nuevos tipos definidos. As´ı, ser´a el propio programa el que realice la tarea de investigar estos tipos y deducir un generador de casos adecuado para cada uno de ellos. Para lograr el segundo en cambio hemos creado una Representaci´on Intermedia (IR) a la que se traducen los programas antes de ser testeados y que permite escribir una plataforma independiente del lenguaje de programaci´on. A su vez profundizaremos en la estructura de clases de CaseGenerator y explicaremos su c´odigo, de manera que queden claras todas las ideas detr´as de su funcionamiento y las razones por las que decidimos utilizar algunas tecnolog´ıas, como la librer´ıa Generics del compilador GHC y la extensi´on de Haskell llamada Template Haskell. 5 Por ´ultimo, tras explicar el funcionamiento de la herramienta expondremos algunos ejemplos pr´acticos del funcionamiento del programa al ser ejecutado con funciones reales. 1.2 Summary One of the most costly parts in software development is testing because it requires a lot of human effort to be able to specify all the test cases launch them and analise all their results. This leads to the problems of most of the programms not being tested as much as it would be necessary. This is the reason why in the last years many testing tools have being developed to automate partialy the testing process. Nevertheless most of them are specialised on a single programming language. Our objective is building a platform that allows tesing applications automatically for the user and that admits as input a program written in any programming language. Inside of this project we will talk about the tool called Case Generator, that is situated inside the CAVI-ART project, being inside of it the part in charge of generating automatically the test cases, adapting them to the needs of each execution. The project takes some ideas used previously in other programms like Quickcheck, Korat or Smallcheck but pursuing the idea of a much automatic process at the same time that it is compatible with several programming languages (functional and nonfunctional ones). To do so our first objective is to get rid of the obligation from the user to define a new generator for each of the newly defined datatypes. Doing so it would be the programm itself the one having to analyze those types and to deduct a generator fiting each of them. In order to be able to do this second change we created an Intermediate Representation (IR) to which all programms are translated before being tested which makes posible to write a plattform independent of all programming languages. In this project we will also explain the class structure of CaseGenerator and it’s code to make clear all the ideas behind it’s behaviour together with why we decided to use some technologies as the library Generics of the GHC compiler and the Haskell extension called Template Haskell. Finally after explaining how the plattform works we will show some examples about the program behaviour while executed with real functions. 1.3 Palabras clave prueba, verificaci´on, autom´atica, caja negra, pruebas basadas en asertos 1.4 Keywords testing, verification, automatic, black box, assertion based testing 6 Cap´ıtulo 2 Preliminares 2.1 Proyecto CAVI-ART En esta secci´on explicamos el proyecto CAVI-ART, actualmente en fase de desarollo en la UCM y del cual forma parte mi TFG. La plataforma CAVI-ART (vease el esquema de la figura 2.1) consiste en un conjunto de herramientas pensadas para ayudar al programador en la validaci´on de programas escritos en diferentes lenguajes. Estas ayudas incluyen la extracci´on autom´atica y prueba de condiciones de verificaci´on, la prueba autom´atica de terminaci´on (siempre que sea decidible usando la tecnolog´ıa actual), la inferencia autom´atica de algunos invariantes y la generaci´on autom´atica y ejecuci´on de casos de prueba. [6, 3, 5] Un aspecto clave de la plataforma es su Representaci´on Intermedia de los programas (de aqu´ı en adelante IR). Los programas escritos en lenguajes convencionales como C++, Java, Haskell, OCaml y otros, se traducen a la IR, sobre la que se realizan todas las actividades mencionadas anteriormente. La intenci´on es programar la mayor parte de la plataforma una sola vez, de manera que sea independiente del lenguaje de programaci´on utilizado. La IR se dise˜n´o con la intenci´on de facilitar al m´aximo posible las tareas nombradas con anterioridad, mediante un dise˜no simple que cuenta con muy pocas construcciones primitivas. Nunca se pens´o en la IR como c´odigo ejecutable sino como una sintaxis abstracta para facilitar el an´alisis est´atico y la verificaci´on formal. Sin embargo en los ´ultimos meses se decidi´o convertir la IR en c´odigo ejecutable, para posibilitar la ejecuci´on de pruebas y construcci´on de herramientas de testeo, ambas independientes del lenguaje. Esto supone una ventaja ya que la mayor´ıa de las herramientas de testeo existentes est´an ligadas a un lenguaje en concreto. La parte del proyecto encargada de traducir la IR a Haskell y hacer ejecutables los asertos se ha realizado dentro del trabajo de fin de grado de Marta Aracil Mu˜noz con t´ıtulo Implementaci´on de asertos ejecutables para una plataforma de verificaci´on que tambi´en se engloba dentro del proyecto CAVI-ART. 7 Figura 2.1: Esquema del proyecto CAVI-ART 2.2 QuickCheck Quickcheck [2] es una herramienta de Haskell pensada para probar funciones escritas en dicho lenguaje sobre un conjunto de casos de prueba generados de manera aleatoria. Dicho programa result´o ser de gran ayuda, pues tiene ideas similares a lo que quer´ıamos conseguir con nuestro proyecto, ya que se trata tambi´en de un sistema de prueba tipo caja negra. Sin embargo presenta algunas diferencias, sobre todo en la generaci´on de los casos de prueba, ya que Quickcheck los genera de manera aleatoria, mientras que nuestro proyecto los generar´a, como veremos, de manera exhaustiva. 2.2.1 Ejemplo de funcionamiento del programa En este caso vamos a trabajar con la siguiente propiedad de las listas, cierta para cualquier lista finita. prop_RevApp xs ys = reverse (xs++ys) == reverse ys++reverse xs Ahora lanzamos el programa Quickcheck para comprobar si supera todos los casos de prueba. 8 Main>QuickCheck prop RevApp OK: passed 100 t e s t s . Veamos ahora que pasa en caso de que nuestra funci´on no est´e definida correctamente. prop_RevApp2 xs ys = reverse (xs++ys) == reverse xs++reverse ys Al ejecutar la nueva funcion desde Quickcheck. Main> quickcheck prop_RevApp2 Falsifiable, after 1 tests: [2] [-2,1] Aqu´ı podemos observar que en caso de fallo Quickcheck nos devuelve el contraejemplo de tama˜no m´ınimo, lo que nos indica esta vez es que nuestra definici´on ha fallado en el primer test y que en dicho caso las respectivas listas para las que ha sido probado falso son [2] y [-2,1]. 2.2.2 Leyes condicionales En algunos casos las leyes que queremos definir no pueden ser representadas mediante una simple funci´on y solo son ciertas bajo unas precondiciones muy concretas. Para dichos casos Quickcheck cuenta con el operador de implicaci´on ==> para representar dichas leyes condicionales. Por ejemplo una ley tan simple como la siguiente: x<= y ==>max x y == y Puede ser representada mediante la siguiente definici´on. prop_MaxLe :: Int -> Int -> Property prop_MaxLe x y = x <= y ==> max x y == y En este ejemplo podemos observar que el resultado de la funci´on es de tipo Property en vez de Boolean, lo cual es debido a que en el caso de las leyes condicionales en vez de probar la propiedad para 100 casos aleatorios, ´esta es probada contra 100 casos que cumplan la precondici´on establecida. Si uno de los candidatos no la cumple ser´a descartado y se considerar´a el siguiente. Quickcheck genera un m´aximo de 1000 casos de prueba y si entre ellos no se han encontrado al menos 100 que cumplan la precondici´on, simplemente informa al usuario cuantos la cumplen. Dicho l´ımite est´a pensado para que en caso de que no existan m´as casos que cumplan dicha precondici´on el programa no busque indefinidamente. 9 16 Cap´ıtulo 3 Nuestra propuesta: las clases Allv, Sized y Arbitrary 3.1 Black box testing en nuestro contexto En el mundo del testing existen dos grandes posibilidades: sistemas de tipo caja negra y sistemas de tipo caja blanca. Los de caja negra son aquellos sistemas de testing que no se basan en la estructura interna, si no que trabajan ´unicamente con la entrada, sobre la que aplican una precondici´on, y la salida sobre la que comprueban si cumple las postcondiciones establecidas. En cambio los de caja blanca no testean ´unicamente las entradas y salidas del programa aplicandoles precondiciones y comprobando la postcondiciones, sino que adem´as se basan en la estructura interna del programa para realizar la generaci´on de casos de prueba, de forma que se cubra todo el texto del programa. Seg´un el criterio de cobertura deseado se pueden generar casos para ejercitar todas las condiciones o todas las ramas o todos los caminos. En el caso de nuestro proyecto nos decidimos por el m´etodo de caja negra, pues quer´ıamos conseguir un sistema v´alido para poder probar cualquier programa sin necesidad de tener que volver a generar los casos de prueba cuando cambia la estructura interna del programa. Esa es una de las desventajas del testeo de tipo caja blanca, que para poder comprobar partes de la estructura interna de un programa tendr´ıamos que adaptar la plataforma para cada uno de los nuevos programas. La idea principal detr´as de nuestro proyecto era principalmente la inmediatez y la comodidad del usuario, es decir que para probar un programa no fuera necesario escribir c´odigo extra, aparte del ya existente programa, sino que solo fuera especificar como quiere que se generen los casos de prueba y los rangos de los dominios a usar y con eso sea ya capaz de probar su programa, lo cual se ajusta mucho m´as a la idea de testeo de caja negra. Las posibles maneras en las que el usuario puede especificar como se generan los casos de prueba para cada argumento son 3: •Generar ncasos de prueba de manera aleatoria. 17 •Coger ncasos de prueba de tama˜no menor o igual a m. •Coger los nprimeros casos de prueba de la lista de todos los valores, sea cual sea su tama˜no. 3.2 Sized En la estructura del proyecto, Sized est´a pensada como la clase externa que hereda de Allv (la cual se puede ver en la figura 3.1). A su vez es la clase que se ocupa de devolver la lista de los casos de prueba a partir de la lista allv de todos los valores de un tipo de datos. Esto se realiza mediante dos funciones: •sized que devuelve los nprimeros casos menores o iguales a un tama˜no m. •smallest que devuelve los nprimeros casos de la lista allv seg´un su posici´on y sin importar su tama˜no. En esta clase del proyecto decidimos implementar el concepto de tama˜no de un elemento mediante la librer´ıa Generics explicada anteriormente, pues de esa manera podr´ıamos tener una representaci´on del tama˜no independiente del tipo y no hay que definirlo para cada tipo nuevo creado por el usuario. En primer lugar debemos definir la clase externa de la parte de Generics que ser´a la que nosotros usemos. En ella, s´olo debemos definir las funciones que queremos que tenga y como se comunica con la clases internas de Generics. Primero definimos la funcion en si, que dada un elemento de un tipo cualquiera nos devuelva un entero que representar´a su tama˜no. Despu´es debemos definir como se comunica la funci´on size externa con la versi´on gen´erica gsize para obtener de esta el valor a devolver. En este caso usamos la funci´on from recibe un valor en su representaci´on no gen´erica y lo transforma a su representaci´on gen´erica para que pueda ser manipulado en las diferentes funciones. En este caso es simple pues el valor del tama˜no obtenido por gsize ser´a el mismo devuelto por nuestra funci´on size. Finalmente creamos la clase interna GSized y definimos la funci´on gsize. Una vez tenemos la interfaz entre las dos clases Sized yGSized lo siguiente que debemos definir es el constructor sin argumentos, que en nuestro caso devuelve el tama˜no 0. A continuacion definimos size para un tipo compuesto por otros dos, el tama˜no de dicho tipo es la suma de los tama˜nos de los tipos que los componen. Tras ello definimos el comportamiento cuando el tipo tiene mas de un constructor posible, en este caso si elegimos el constructor de la derecha el tama˜no del tipo ser´a el del tipo de la derecha y similar si elegimos el constructor de la izquierda. Por ´ultimo, tenemos la instancia utilizada para trabajar con la metainformaci´on del tipo, que en nuestro caso al no ser necesaria dicha informaci´on simplemente llamamos de nuevo a la funcion gsize ignorando la metainformaci´on. 18 Figura 3.1: Clase Sized 3.3 Allv/TemplateAllv En primer lugar vamos a tratar la clase Allv, cuyas instancias cuentan unicamente con una funci´on, allv la cual devuelve la lista de todos los posibles valores del tipo de datos en orden creciente de tamaos. Al principio esta clase estaba pensada para ser una ´unica clase que utilizara la librer´ıa Generics y para contar con un m´etodo, compose (su funcin se explica ms adelante) con el cual ser capaces de generar instancias de la clase Allv para los tipos definidos por el usuario. Dicha funci´on se encargar´ıa de crear la lista de todos los valores (allv) para el nuevo tipo de datos a partir de las listas de los tipos predefinidos, pero a la hora de integrarlo con la clase Sized encontramos un problema. La idea que ten´ıamos sobre esta clase era darle al usuario la posibilidad de pedir los nvalores mas 19 peque˜nos de una clase o los nprimeros valores de tama˜no menor o igual a un n´umero prefijado por ´el. Lo cual entraba en conflicto con la manera en la que gener´abamos las listas de allv para los tipos definidos por el usuario. Dadas dos listas la idea es realizar el producto cartesiano de ellas siendo este el resultado de generar todas las parejas con un valor de la primera lista y otro de la segunda. Teniendo en cuenta que ambas pueden ser infinitas, dicho producto deber´a ser realizado por diagonales, mostramos la idea en la figura 3.2. La combinaci´on de listas infinitas pod´ıa ser realizada sin problemas usando Generics, pero el problema llegaba a la hora de querer devolver los nprimeros valores de un tama˜no menor o igual am, ya que para ello deb´ıamos ordenar la lista infinita y encontramos el problema de que en dichas listas infinitas el n´umero de elementos de un tama˜no dado siempre es infinito y que siempre hay alg´un elemento m´as de tama˜no menor o igual a m, aunque est despu´es de muchos elementos intermedios que no lo son. Existe un segundo problema que es el del orden de los constructores, ya que debemos garantizar que en la unin de dos alternativas los casos base se generan antes que los recursivos. Estos problema nos hicieron pensar en utilizar Template Haskell en lugar de Generics. En la versi´on definitiva del programa en el mdulo TemplateAllv se encuentra esta funcionalidad de crear una instancia de Allv para los tipos de datos definidos por el usuario, utilizando para ello gen allv, con la ayuda de la ya nombrada funci´on compose (su cdigo se muestra en la figura 3.3). La funci´on compose se encarga de concatenar todas las diagonales en una ´unica lista final, que es la que se devuelve mediante la funci´on allv, por otro lado diags se encarga de crear una de las diagonales y mientras no sea la ´ultima y de volver a llamarse a s´ı misma con los par´ametros para la siguiente. Los par´ametros de la funci´on diags son: •ise trata del ordinal de la diagonal que vamos a generar. •xs eys se tratan de las dos listas que vamos a combinar. Adem´as, dentro de TemplateAllv existen tres funciones que se encargan de crear una instancia adecuada de la clase Allv para cada uno de los tipos de datos definidos por el usuario. La primera de ellas, y la m´as externa en dicho proceso es gen allv, la cual adem´as de llamar a typeInfo para extraer la informaci´on del tipo y pasarsela a las subfunciones, es tambi´en en la que se define, dentro de gen body, como se formar´a exactamente la nueva funci´on allv para la instancia del tipo. Los restantes detalles sobre gen allv pueden verse en el cdigo que se adjunta en el apndice, apartado 8.3. La siguiente funci´on a tratar, gen instance 8.3 se encarga de crear una instancia de la clase Allv para el nuevo tipo de datos (par´ametro for type) y adjuntar a dicha instancia la definici´on de la funci´on allv que se crea en gen clause. Por ´ultimo tenemos la funci´on gen clause que es responsable de crear la definici´on de la funci´on allv para el tipo de datos, usando para ello la funci´on gen body que hab´ıa sido definida anteriormente en gen allv. Adem´as, cuenta con una serie de funciones auxiliares que realizan parte del procesamiento: 20 •listOfFOut se encarga de crear la lista de nombres de variables entre f1yfn para aquellos casos en los cuales los constructores tienen m´as de un par´ametro. •isRec devuelve una lista de booleanos en la cual cada posici´on indica si el constructor en dicha posici´on es recursivo o no. •reorderL sirve para reordenar los constructores (lo cual es equivalente a las listas con la informaci´on por cada constructor) de manera que queden en primer lugar aquellos que no son recursivo y al final los que si lo son. Esto es necesario, ya que los constructores recursivos har´an uso de aquellos que no lo son y por ello los no recursivos deben definirse en primer lugar. •gen wheres que es responsable de definir las clausulas where necesarias para todos aquellos constructores con m´as de un par´ametro que necesiten utilizar una funci´on auxiliar (que son las representadas por las f’s). •tupleParam crea las tuplas de par´ametros para cada una de las funciones auxiliares f. 3.4 Instancias predefinidas En este ´ultimo apartado mostramos las instancias dentro de las clases Sized yAllv para los tres tipos b´asicos (Int,CharyBool) y para los tipos que se deducen directamente de ellos, como es el caso de listas de cualquier tipo ya instanciado en dichas clases o las tuplas de hasta longitud 6. (El cdigo correspondiente a dichas instancias se adjunta en el apndice, apartado 8.1) Como podemos observar en el caso de la instancia en la clase Sized, cualquier elemento de uno de los tres tipos tendr´a tama˜no uno. En el caso de las instancias de los tres tipos en la clase Allv, simplemente debemos indicar el conjunto de valores de dicha clase que ser´an elegibles a la hora de generar casos de prueba, para las cuales utilizamos la funci´on de compose explicada con anterioridad. En el caso de las instancias derivadas dentro de la clase Sized ´estas se generan mediante Generics. 21 Figura 3.2: Esquema funcionamiento compose 22 Figura 3.3: Funci´on compose 23 24 Cap´ıtulo 4 El generador de casos 4.1 La interfaz con la UUT En este cap´ıtulo vamos a tratar las diferentes fases del proceso de testeo por las que pasa el programa, utilizando para ello un ejemplo de funcionamiento, en este caso una funci´on insert en una lista ordenada. En primer lugar vamos a echar un ojo a la Unit Under Testing (a partir de ahora UUT) que se trata de la clase que contiene toda la informaci´on sobre la funci´on que vamos a testear en cada momento. Podemos observar la forma que tiene en la figura 4.1. Este archivo Haskell en el caso de nuestro programa es sintetizado a partir de la funci´on proporcionada por el usuario utilizando la herramienta IR2Haskell mencionada en la secci´on 2.1 y podemos observar que incluye: •uutName indica el nombre de la funci´on a testear para efectos de nombrarla cuando se presentan los resultados al usuario •Por ultimo las tres funciones uutPrec,uutMethod yuutPost acompa˜nadas de las funciones auxiliares necesarias. En caso de que las funciones utilizaran alg´un tipo de datos definido por el usuario su definici´on se incluir´ıa tambien en el archivo UUT. 4.2 La obtenci´on del tipo de la UUT El siguiente paso analiza los tipos de los par´ametros de entrada de la funci´on que queremos probar, de esa manera podremos generar casos de prueba para dichos tipos de datos. Nos basaremos para ver el proceso en el ejemplo de insert comenzado en el apartado anterior. Este proceso se realiza mediante la funci´on get f inp types y sus funciones auxiliares, cuyo c´odigo puede encontrarse en la primera parte del ap´endice. 25 Figura 5.1: Casos de la primera prueba que pasaron la precondici´on 5.3 Insertar un elemento en un ´arbol Funci´on: insertBST x Precondici´on: P rec(x, t) = sorted(inorder(t)) es decir, la propiedad de ser un ´arbol de b´usqueda Postcondici´on: P ost(x, t, res) = sorted(inorder(res))permut(x:inorder(t), inorder(res)), es decir ambas listas tienen los mismos elementos Se generaron para probar dicha funci´on un total de 1000 casos de prueba, de los cuales pasaron la precondici´on un total de 518 casos de prueba. De todos esos casos de prueba que pasaron la precondici´on todos ellos pasaron la postcondici´on, no encontramos casos que la contradijeran. 5.4 B´usqueda en un ´arbol Funci´on: search x t Precondici´on: P rec(x, t) = sorted(inorder(t)) es decir, la propiedad de ser un ´arbol de b´usqueda Postcondici´on: P ost(x, t, res) = res ↔x∈inorder(t) es decir, el resultado es cierto 32 si, y solo si, x pertenece al ´arbol t Se generaron para probar dicha funci´on un total de 1000 casos de prueba, de los cuales pasaron la precondici´on un total de 518 casos de prueba. De todos esos casos de prueba que pasaron la precondici´on 45 de ellos no pasaron la postcondici´on. 5.5 Conclusiones de los experimentos En las cuatro pruebas podemos observar que de los 1000 ejemplos generados, en todos ellos un porcentaje razonable pasa la precondici´on, incluso en el segundo caso que es el que cuenta con una precondici´on m´as fuerte. En los tres casos en los cuales la definici´on de la funci´on, su precondici´on y postcondici´on son correctas nuestro programa no detecta ningun error, todos lo casos de prueba que cumplen la precondici´on son aceptados como correctos, en cambio en el ´ultimo de los casos, el cual fue definido incorrectamente a prop´osito el programa detecta que est´a definido incorrectamente con una buena cantidad de contraejemplos, cerca de un 10% de los casos que pasaron la precondici´on. 33 34 Cap´ıtulo 6 Trabajo relacionado y conclusiones 6.1 Korat La primera de las herramientas que vamos a tratar en este apartado es Korat [1], una herramienta de Java que sirve para la generaci´on de casos complejos de prueba a partir de unas restricciones dadas. La idea detr´as de Korat es que dado un predicado en Java y una funci´on finitialization en la cual definimos los dominios para cada una de las clases del input, es decir los valores v´alidos para cada una de ellas, explora el espacio de estados de las posibles soluciones generando s´olo soluciones no-isomorficas entre si, de esta manera consigue una gran poda de las soluciones no interesantes del espacio de b´usqueda. Lo primero que hace Korat es reservar el espacio necesario para los objetos especificados, en el caso de un BinTree reservaria espacio para ´el y para el n´umero de Nodos que queramos. Por ejemplo, si queremos un ´arbol con tres nodos el vector contendr´ıa 8 campos: •2 para el BinTree (uno para la ra´ız y otro para el tama˜no). •2 campos por cada uno de los 3 nodos (hijo izquierdo/hijo derecho). Cada uno de los posibles candidatos que considere Korat a partir de ese momento ser´a una evaluaci´on de esos 8 campos. Por lo tanto el espacio de estados de b´usqueda del input consiste en todas las posibles combinaciones de esos campos, donde cada uno de ellos toma valores de su dominio definido en finitialization. Para conseguir explorar de manera sistem´atica y completa el espacio de estados, Korat ordena todos los elementos en los dominios de las clases y los dominios de los campos. Dicho orden dentro de cada uno de los dominios de los campos ser´a consistente con el del dominio de la clase y todos los valores que pertenezcan al mismo dominio de clase ocurriran de manera consecutiva en el dominio del campo. 35 Tras esto, cada candidato de la entrada se respresenta como un vector de ´ındices de sus correspondientes dominios de campos. Tras definir los dominios de cada uno de los campos del vector comienza la busqueda con la inicializaci´on a 0 de todos los indices del vector. A continuaci´on fijamos los valores de los campos para cada posible candidato de acuerdo a los valores en el vector y acto seguido invoca a la funcion repOk que es donde el usuario ha definido la precondici´on. Durante dicha ejecuci´on Korat monitoriza el orden en que son accedidos los campos del vector y construye una lista con los identificadores de los campos, ordenados por la primera vez en que repOk los accede. Cuando repOk retorna Korat genera el siguiente candidato incrementando el ´ındice del dominio de campo para el campo que se encuentra ´ultimo en la lista ordenada construida previamente. Si dicho ´ındice es mayor que el tama˜no del dominio de su campo, este se pone a cero y se incrementa el ´ındice de la posici´on anterior y as´ı sucesivamente. Al seguir este m´etodo para generar el siguiente candidato conseguiremos podar un gran n´umero de ellos que tienen la misma evaluaci´on parcial sin dejar fuera ninguno v´alido. El algoritmo de busqueda descrito aqu´ı genera las entradas en orden lexicogr´afico. Adem´as, para los casos en los que repOk no es determinista, este m´etodo garantiza que son generados todos los candidatos para los que repOk devuelve True. Los casos para los que siempre devuelve False nunca son generados y los casos para los que alguna vez se devuelve True y otras veces False pueden ser generados o no. Dos candidatos ser´an definidos como isomorfos si las partes de sus grafos alcanzables desde la ra´ız son isomorfas. En el caso de repOk el objeto ra´ız es aquel pasado como argumento impl´ıcito. El isomorfismo entre candidatos divide el espacio de estados en particiones isom´orficas (debido al ordenamiento lexicogr´afico introducido por el orden de los valores de los dominios de los campos y la ordenaci´on de los campos realizado por repOk). Para cada una de dichas particiones isomomorficas Korat genera ´unicamente el candidato lexicogr´aficamente menor. Adem´as, con el proceso explicado anteriormente para generar el siguiente candidato, teniendo en cuenta la lista de ordenaci´on de los campos, Korat se asegura de no generar varios candidatos dentro de la misma partici´on isom´orfica. 6.2 Smallcheck La segunda herramienta a tratar en este apartado es Smallcheck [7] una librer´ıa para Haskell usada en el testing basado en propiedades. Esta librer´ıa parte de las ideas del Quickcheck y perfecciona algunos de los puntos flacos de este. La principal diferencia de Smallcheck respecto a Quickcheck es la forma en que genera sus casos de prueba. En este caso Smallcheck se apoya en la ”hip´otesis del ´ambito peque˜no” la cual dice que si un programa no cumple su especificaci´on en alguno de sus casos casi siempre existir´a un caso simple en el cual no la cumpla o lo que viene a ser lo mismo, que si un programa no falla en casos peque˜nos lo normal es que no falle en ninguno de sus casos. 36 Partiendo de esta idea cambia la generaci´on existente en Quickcheck, que era aleatoria, por una generaci´on exhaustiva de todos los casos de prueba peque˜nos, ordenados por profundidad (que es el nombre usado para el tama˜no), dejando a criterio del usuario hasta que profundidad deben considerarse como peque˜nos. A continuaci´on presentaremos como est´an definidas las profundidades m´as importantes: •En el caso de los tipos de datos algebraicos, como es usual, la profundidad de una construcci´on de aridad cero es cero mientras que la profundidad de una construcci´on de aridad positiva es una m´as que la mayor de todos sus argumentos. •En el caso de las tuplas, dicha profundidad se define de manera un poco diferente. La profundidad de una tupla de aridad cero es cero pero la de una tupla de aridad positiva es la mayor profundidad de entre todas las de sus componentes. •En el caso de los tipos num´ericos, la definici´on de la profundidad se realiza con respecto a una representaci´on imaginaria como una estructura de datos. De esta manera, la profundidad de un entero iser´a su valor absoluto, ya que se construy´o de manera algebraica como SucciZero. A su vez, la profundidad de un numero decimal sx2ees la de la tupla de enteros (s,e). Smallcheck define una clase Serial de tipos que pueden ser enumerados hasta una determinada profundidad. Existen instancias predefinidas de la clase Serial para todos los tipos de datos del preludio . Sin embargo, es muy f´acil definir una nueva instancia de dicha clase para un tipo de datos algebraico, ´esta es de un conjunto de combinadores cons<N>, gen´ericos para cualquier combinaci´on de tipos Serial, donde Nes la aridad del constructor. Supongamos un tipo de datos en Haskell Prop en el que tenemos una variable, la negaci´on de una variable y el Or de dos variables. data Prop = Var Name |Not Prop |Or Prop Prop Para dicho tipo de datos definir una instancia de la clase Serial, asumiendo una definici´on similar para el tipo Name, ser´ıa. in sta nce S e r i a l Prop where s e r i e s = cons1 Var \/ cons1 Not \/ cons2 Or Una serie es simplemente una funci´on que dado un entero devuelve una lista finita. type S e r i e s a = Int −>[a] A su vez el producto y la suma sobre dos series se definen como: (\/) : : S e r i e s a −>Series a −>Series a s1 \/ s2 = \d−>s1 d ++ s2 d (><) : : S e r i e s a −>Series b −>S e r i e s ( a , b) s1 >< s2 = \d−>[ ( x , y ) |x<−s1 d , y <−s2 d ] 37 Por ´ultimo, los combinadores cons<N> est´an definidos usando >< decrementando y comprobando la profundidad correctamente. cons0 c = \d−>[c] cons1 c = \d−>[ c a |d>0 , a <−series (d−1)] cons2 c = \d−>[ c a b |d>0 , (a , b) <−(series >< series) (d−1)] Cuando se usa muchas veces el esquema general para definir valores de prueba se produce que para alguna profundidad peque˜na dlos 10.000-100.000 casos de prueba son comprobados r´apidamente, pero para la profundidad d+1 resulte imposible completar los miles de millones de casos de prueba. Por ello, resulta necesario reducir algunas dimensiones del espacio de b´usqueda de manera que otras de las dimensiones puedan ser comprobadas en mayor profundidad. El primer punto a tener en cuenta es, que a pesar de que los n´umeros enteros pueden parecer una elecci´on obvia como valores base para las pruebas, debemos considerar que los espacios de busqueda para los tipos compuestos (especialmente funcionales) al usar bases num´ericas, crecen de manera muy r´apida. En muchos casos el tipo booleano puede ser una elecci´on perfectamente v´alida para los valores base, y con ello se conseguir´oa reducir en gran medida el espacio de busqueda respecto a la utilizaci´on de enteros. Existe otra versi´on de Smallcheck llamada Lazy Smallcheck, que a su vez se aprovecha de la evaluaci´on perezosa de Haskell, la cual permite que una funci´on devuelva un valor, aunque esta est´e aplicada sobre una entrada definida parcialmente. Esta posibilidad de obtener el resultado de una funci´on sobre muchas entradas en una sola ejecuci´on, puede resultar de gran ayuda en el testeo basado en propiedades, ya que si una funci´on se cumple para una soluci´on parcial, esta se cumplir´a para todas las funciones totalmente definidas que partan de la misma. En eso se centra el Lazy Smallcheck, en evitar generar todas esas funciones totalmente definidas que no aportan nada de informaci´on extra sobre la definici´on parcial. La actual versi´on de Lazy Smallcheck es capaz de testear propiedades de primer orden con o sin cuantificadores universales. 38 Cap´ıtulo 7 Conclusiones del proyecto 7.1 Conclusiones La idea de generar valores para tipos de datos predefinidos y definidos por el usuario mediante el uso de las clases de Haskell ya est´a presente tanto de Quickcheck como en Smallcheck. La idea de generar casos de prueba exhaustivos hasta un cierto tama˜no, tambi´en est´a presente tanto en Smallcheck como en Korat. La diferencia principal de nuestro trabajo con estos es que los tres requieren que el usuario escriba c´odigo adicional para los tipos del usuario que son desconocidos para el sistema. En el caso de Quickcheck, hay que generar manualmente la instancia de la clase Arbitrary, si bien el sistema ofrece una serie de combinadores que facilitan la tarea. En el caso de Smallcheck, hay que escribir manualmente una instancia de la clase Serial, y en el caso de Korat hay que editar una plantilla para definir una noci´on de tama˜no y para evitar generar valores duplicados. En nuestro trabajo, tanto la noci´on de tama˜no, como las instancias de la clases Allv y Sized, se generan autom´aticamente para los tipos desconocidos, gracias al uso de respectivamente Template Haskell y Generics. Ello unido a que el c´odigo de la precondicion y la postcondici´on son generados autom´aticamente por la herramienta previa IR2Haskell, hace que toda el proceso de prueba desde que el usuario escribe su c´odigo y asertos originales, hasta que se ejecutan las pruebas y se detectan los posibles errores, se haga sin ninguna intervenci´on manual. Durante la creaci´on de los experimentos reportados en este trabajo, la herramienta fue capaz de detectar errores no intencionados, tanto en las postcondiciones inicialmente escritas, como en el c´odigo bajo prueba, lo cual a la vez sirvi´o para asegurarnos de que la herramienta detecta de manera correcta errores en la definici´on de la funci´on. 7.2 Conclusions The idea of generating values both for the predefined datatypes and the types defined by the user using Haskell classes is already present both in Quickcheck and 39 Smallcheck. The idea about genrating exhaustive test cases to a certain size is also present both in Smallcheck and Korat. The main difference between our project and all those projects are that those three need the user to write additional code for the user-defined datatypes that are not know by the system. In Quickcheck is necessary to manually generate instance for the Arbitrary class using a set of combiners given to do so. In the case of Smallcheck it’s necessary to manually create an instance for the Serial class and in Korat you have to edit a template to define the concept of size and being able to avoid duplicated values. In our project, both the concept of size and the instances of Allv and Sized classes are automatically generated for all the unknown data types thanks to Template Haskell and Generics. This together with the fact that the code for the precondition and postcondition are automatically generated by the tool IR2Haskell makes all the testing process, from the moment in which the user writes its code and asserts until the moment in which tests are executed and the possible errors are detected flow without any intervention from the user. During the creation of the experiments shown in this project, the tool was able to find some non intended errors both in some firstly writen postconditions and code under test, which served us to be completely sure about the correct functioning of the tool as it was able to detect incorrectness in the function definition 40 Cap´ıtulo 8 Ap´endice 8.1 Instancias predefinidas -- | For basic types we must give the instances instance Sized Int where size x = 1 instance Allv Int where allv = [1..5] instance Sized Char where size x = 1 instance Allv Char where allv = [’a’..’z’] instance Sized Bool where size x = 1 instance Allv Bool where allv = [True, False] instance Sized a => Sized [a] instance (Sized a, Sized b) => Sized (a,b) instance (Sized a, Sized b, Sized c) => Sized (a,b,c) instance (Sized a, Sized b, Sized c, Sized d) => Sized (a,b,c,d) instance (Sized a, Sized b, Sized c, Sized d, Sized e) => Sized (a,b,c,d,e) 41 8.5 UUTs de los diferentes casos de prueba 8.5.1 Insertar en una lista ordenada module UUT where import qualified Arrays as A import qualified Bags as B import qualified Sets as S import qualified Sequences as Q import Assertion import Data.List uutNargs :: Int uutNargs = 2 uutMethods :: [String] uutMethods = ["uutPrec", "uutMethod", "uutPost"] uutName :: String uutName = "insert" uutPrec :: Int -> [Int] -> Bool uutPrec x xs = sorted xs sorted [] = True sorted [x] = True sorted (x:y:xs) = x <= y && sorted (y:xs) uutMethod :: Int -> [Int] -> [Int] uutMethod x [] = [x] uutMethod x (y:ys) | x <= y = x:y:ys | otherwise = y : uutMethod x ys uutPost :: Int -> [Int] -> [Int] -> Bool uutPost x xs ys = ys == sort (x:xs) 8.5.2 Insertar en un Array module UUT where import qualified Arrays as A import qualified Bags as B import qualified Sets as S import qualified Sequences as Q import Assertion 48 import Data.List uutNargs :: Int uutNargs = 3 uutMethods :: [String] uutMethods = ["uutPrec", "uutMethod", "uutPost"] uutName :: String uutName = "insert" --TODO usar al principio del output uutPrec x m a = evalA $ And (FTerm (Aplic (Aplic (TVar (<=)) ((TConst 0))) ((TVar m)))) (And (FTerm (Aplic (Aplic (TVar (<)) ((TVar m))) (Aplic ((TVar A.len)) ((TVar a))))) (Forall (GuardIntTuple (Tuple2 ((TConst 0)) ((TConst 0))) (Tuple2 (Aplic (Aplic (TVar (-)) (TVar m)) (TConst 1)) (Aplic (Aplic (TVar (-)) (TVar m)) (TConst 1)))) (\(i, j) -> (Imp (FTerm (Aplic (Aplic (TVar (<=)) ((TConst 0))) ((TVar i)))) (Imp (FTerm (Aplic (Aplic (TVar (<=)) ((TVar i))) ((TVar j)))) (Imp (FTerm (Aplic (Aplic (TVar (<)) ((TVar j))) ((TVar m)))) (FTerm (Aplic 49 (Aplic (TVar (<=)) (Aplic (Aplic ((TVar A.get)) ((TVar a))) ((TVar i)))) (Aplic (Aplic ((TVar A.get)) ((TVar a))) ((TVar j))))))))))) uutMethod x m a = let i = (-) m 1 in f2xmia where f2xmia= let b1 = (>=) i 0 in case b1 of False -> f4 x m i a True -> let e = A.get a i in let b2 = (<) x e in case b2 of True -> let e = A.get a i in let i2 = (+) i 1 in let ap = A.set a i2 e in let i3 = (-) i 1 in f2 x m i3 ap False -> f4 x m i a f4xmia= let i2 = (+) i 1 in let ap = A.set a i2 x in ap uutPost x m a res = evalA $ Forall (GuardIntTuple (Tuple2 ((TConst 0)) ((TConst 0))) (Tuple2 ((TVar m)) ((TVar m)))) (\(i, j) -> (Imp (FTerm (Aplic (Aplic (TVar (<=)) ((TConst 0))) ((TVar i)))) (Imp (FTerm (Aplic (Aplic (TVar (<=)) ((TVar i))) 50 ((TVar j)))) (Imp (FTerm (Aplic (Aplic (TVar (<=)) ((TVar j))) ((TVar m)))) (FTerm (Aplic (Aplic (TVar (<=)) (Aplic (Aplic ((TVar A.get)) ((TVar res))) ((TVar i)))) (Aplic (Aplic ((TVar A.get)) ((TVar res))) ((TVar j))))))))) 8.5.3 Insertar en un ´arbol -- This file has been generated by the CAVI-ART CLIR-to-Haskell transformer tool -# LANGUAGE DeriveGeneric #- module UUT where import qualified Arrays as A import qualified Bags as B import qualified Sets as S import qualified Sequences as Q import Assertion import Data.List import GHC.Generics -- Inserting in a Binary Search tree -- This is an example where the user defines a new type data Tree a = Empty | Node (Tree a) a (Tree a) deriving (Generic,Show,Eq) uutNargs :: Int uutNargs = 2 uutMethods :: [String] uutMethods = ["uutPrec", "uutMethod", "uutPost"] uutName :: String 51 uutName = "insertBST" uutPrec :: Int -> Tree Int -> Bool uutPrec x t = sorted $ inorder t inorder Empty = [] inorder (Node l x r) = inorder l ++ (x : inorder r) sorted [] = True sorted [x] = True sorted (x:y:xs) = x <= y && sorted (y:xs) uutMethod :: Ord a => a -> Tree a -> Tree a uutMethod x Empty = Node Empty x Empty uutMethod x t@(Node l y r) | x < y = Node (uutMethod x l) y r |x==y=t | x > y = Node l x (uutMethod x r) uutPost x t o = if x ‘elem‘ inorder t then t == o else inorder o == sort (x : inorder t) 8.5.4 B´usqueda en un ´arbol -# LANGUAGE DeriveGeneric #- module UUT where import qualified Arrays as A import qualified Bags as B import qualified Sets as S import qualified Sequences as Q import Assertion import GHC.Generics -- Searching in a Binary Search tree -- This is an example where the user defines a new type data Tree a = Node (Tree a) a (Tree a) | Empty deriving (Generic,Show) uutNargs :: Int 52 uutNargs = 2 uutMethods :: [String] uutMethods = ["uutPrec", "uutMethod", "uutPost"] uutName :: String uutName = "searchBST" uutPrec :: Int -> Tree Int -> Bool uutPrec x t = sorted $ inorder t inorder Empty = [] inorder (Node l x r) = inorder l ++ (x : inorder r) sorted [] = True sorted [x] = True sorted (x:y:xs) = x <= y && sorted (y:xs) uutMethod :: Ord a => a -> Tree a -> Bool uutMethod x Empty = False uutMethod x t@(Node l y r) | x < y = uutMethod x r -- error, deber´ıa ser l | x == y = True | x > y = uutMethod x r uutPost x t o = o == (x ‘elem‘ inorder t) 53 54 Bibliograf´ıa [1] Chandrasekhar Boyapati, Sarfraz Khurshid & Darko Marinov (2002): Korat: Automated Testing Based on Java Predicates. Available at http://web.eecs.umich.edu/ bchandra/publications/issta02.pdf. [2] Koen Claessen & AJohn Hughes (2000): QuickCheck:A Lightweight Tool for Random Testing of Haskell Programs. Available at https://www.eecs.northwestern.edu/ robby/courses/395-495-2009-fall/quick.pdf. [3] Moreno Falaschi, editor (2015): Logic-Based Program Synthesis and Transformation - 25th International Symposium, LOPSTR 2015, Siena, Italy, July 13-15, 2015. Revised Selected Papers.Lecture Notes in Computer Science 9527, Springer, doi:10.1007/978-3-319-27436-2. Available at http://dx.doi.org/10.1007/978-3-319-27436-2. [4] Magalhaes, Atze Dijkstra, Johan Jeuring & Andres Lh (2010): A Generic Deriving Mechanism for Haskell. Available at http://www.dreixel.net/research/pdf/gdmh nocolor.pdf. [5] Manuel Montenegro, Susana Nieva, Ricardo Pe˜na & Clara Segura (2016): Extending Liquid Types to Arrays. In: PROLE 2016, Salamanca, Spain, pp. 1–15. [6] Manuel Montenegro, Ricardo Pe˜na & Jaime S´anchez-Hern´andez (2015): A Generic Intermediate Representation for Verification Condition Generation. In: Logic-Based Program Synthesis and Transformation - 25th International Symposium, LOPSTR 2015, Siena, Italy, July 13-15, 2015. Revised Selected Papers, pp. 227–243. [7] Colin Runciman, Matthew Naylor & Fredrik Lindblad (2008): SmallCheck and Lazy SmallCheck automatic exhaustive testing for small values. Available at https://pdfs.semanticscholar.org/2460/c9b40ea3c4bbaef53c5f4ad2717154cf15b5.pdf. [8] Tim Sheard & Simon Peyton Jones (2002): Template Meta-programming for Haskell. Available at https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/meta-haskell.pdf. 55