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

Implemen ación de una he amien a de p uebas basadas en ase os pa a una pla a o ma de e i icación Au o : Ped o Ga cía Cas illo Di ec o : Rica do Peña Ma í Facul ad de In o má ica Uni e sidad Complu ense de Mad id Cu so 2016-2017 13 de sep iemb e de 2017 2 ´ Indice 1 Resumen 5 1.1 Resumen................................... 5 1.2 Summa y .................................. 6 1.3 Palab ascla e................................ 6 1.4 Keywo ds .................................. 6 2 P elimina es 7 2.1 P oyec oCAVI-ART............................ 7 2.2 QuickCheck................................. 8 2.2.1 Ejemplo de uncionamien o del p og ama . . . . . . . . . . . . 8 2.2.2 Leyes condicionales . . . . . . . . . . . . . . . . . . . . . . . . . 9 2.2.3 Moni o izando los da os . . . . . . . . . . . . . . . . . . . . . . 10 2.2.4 Como de ini gene ado es . . . . . . . . . . . . . . . . . . . . . 10 2.3 Lib e ´ıa Gene ics de GHC . . . . . . . . . . . . . . . . . . . . . . . . . 11 2.4 Templa eHaskell.............................. 13 2.4.1 Un ejemplo de la idea b´asica . . . . . . . . . . . . . . . . . . . 13 2.4.2 Como usa empla e Haskell . . . . . . . . . . . . . . . . . . . . 13 2.4.3 Rei ica ion (Cosi icaci´on) . . . . . . . . . . . . . . . . . . . . . 14 3 Nues a p opues a: las clases All , Sized y A bi a y 17 3.1 Black box es ing en nues o con ex o . . . . . . . . . . . . . . . . . . 17 3.2 Sized..................................... 18 3.3 All /Templa eAll ............................. 19 3.4 Ins ancias p ede inidas . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 4 El gene ado de casos 25 4.1 Lain e azconlaUUT .......................... 25 4.2 La ob enci´on del ipo de la UUT . . . . . . . . . . . . . . . . . . . . . 25 4.3 La gene aci´on de ins ancias de All y Sized . . . . . . . . . . . . . . . 26 4.4 La gene aci´on y ejecuci´on de casos . . . . . . . . . . . . . . . . . . . . 27 3 5 Expe imen os 31 5.1 Inse a un elemen o en una lis a . . . . . . . . . . . . . . . . . . . . . 31 5.2 Inse a un elemen o en un A ay . . . . . . . . . . . . . . . . . . . . . 31 5.3 Inse a un elemen o en un ´a bol . . . . . . . . . . . . . . . . . . . . . 32 5.4 B´usqueda en un ´a bol . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 5.5 Conclusiones de los expe imen os . . . . . . . . . . . . . . . . . . . . . 33 6 T abajo elacionado y conclusiones 35 6.1 Ko a .................................... 35 6.2 Smallcheck ................................. 36 7 Conclusiones del p oyec o 39 7.1 Conclusiones ................................ 39 7.2 Conclusions................................. 39 8 Ap´endice 41 8.1 Ins ancias p ede inidas . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 8.2 Ob enci´on del ipo de la UUT . . . . . . . . . . . . . . . . . . . . . . . 42 8.3 Gene aci´on de ins ancias de All . . . . . . . . . . . . . . . . . . . . . 44 8.4 Gene aci´on y ejecuci´on de casos . . . . . . . . . . . . . . . . . . . . . . 47 8.5 UUTs de los di e en es casos de p ueba . . . . . . . . . . . . . . . . . 48 8.5.1 Inse a en una lis a o denada . . . . . . . . . . . . . . . . . . . 48 8.5.2 Inse a en un A ay . . . . . . . . . . . . . . . . . . . . . . . . 48 8.5.3 Inse a en un ´a bol . . . . . . . . . . . . . . . . . . . . . . . . 51 8.5.4 B´usqueda en un ´a bol . . . . . . . . . . . . . . . . . . . . . . . 52 4 Cap´ı ulo 1 Resumen 1.1 Resumen Una de las pa es m´as cos osas den o del desa ollo de p og amas es el es eo, ya que equie e un g an es ue zo humano pa a pode especi ica los di e en es casos de p ueba, lanza los y analiza los esul ados. Ello p o oca que en la mayo ´ıa de los casos los p og amas se p ueben mucho menos a ondo de lo que se ´ıa necesa io. Po ello, en los ´ul imos a˜nos han sido desa olladas di e sas he amien as pa a au oma iza de mane a pa cial dicho p oceso de es eo. Sin emba go la mayo ´ıa de ellas es ´an especializadas en un ´unico lenguaje de p og amaci´on. Nues o obje i o es consegui una pla a o ma que pe mi a el es eo de aplicaciones de mane a au om´a ica pa a el usua io y que admi a como en ada un p og ama esc i o en cualquie lenguaje de p og amaci´on. En es e abajo amos a p esen a la he amien a Case Gene a o , que se en- globa den o del p oyec o CAVI-ART, siendo es a pa e la enca gada de gene a los casos de p ueba de mane a au oma izada, adap ´andolos a las necesidades de cada ejecuci´on. Es e p oyec o oma como base las ideas desa olladas an e io men e po p og amas como Quickcheck, Ko a o Smallcheck, pe o in en ando consegui que el p oceso de p ueba sea m´as au om´a ico, y a la ez compa ible con di e sos lenguajes de p og amaci´on an o uncionales como no uncionales. Pa a log a el p ime obje i o hemos eliminado la obligaci´on de que el usua io de ina un nue o gene ado pa a cada uno de los nue os ipos de inidos. As´ı, se ´a el p opio p og ama el que ealice la a ea de in es iga es os ipos y deduci un gene ado de casos adecuado pa a cada uno de ellos. Pa a log a el segundo en cambio hemos c eado una Rep esen aci´on In e media (IR) a la que se aducen los p og amas an es de se es eados y que pe mi e esc ibi una pla a o ma independien e del lenguaje de p og amaci´on. A su ez p o undiza emos en la es uc u a de clases de CaseGene a o y expli- ca emos su c´odigo, de mane a que queden cla as odas las ideas de ´as de su un- cionamien o y las azones po las que decidimos u iliza algunas ecnolog´ıas, como la lib e ´ıa Gene ics del compilado GHC y la ex ensi´on de Haskell llamada Templa e Haskell. 5 Po ´ul imo, as explica el uncionamien o de la he amien a expond emos algunos ejemplos p ´ac icos del uncionamien o del p og ama al se ejecu ado con unciones eales. 1.2 Summa y One o he mos cos ly pa s in so wa e de elopmen is es ing because i equi es a lo o human e o o be able o speci y all he es cases launch hem and analise all hei esul s. This leads o he p oblems o mos o he p og amms no being es ed as much as i would be necessa y. This is he eason why in he las yea s many es ing ools ha e being de eloped o au oma e pa ialy he es ing p ocess. Ne e heless mos o hem a e specialised on a single p og amming language. Ou objec i e is building a pla o m ha allows esing applica ions au oma ically o he use and ha admi s as inpu a p og am w i en in any p og amming language. Inside o his p ojec we will alk abou he ool called Case Gene a o , ha is si ua ed inside he CAVI-ART p ojec , being inside o i he pa in cha ge o gene a ing au oma ically he es cases, adap ing hem o he needs o each execu ion. The p ojec akes some ideas used p e iously in o he p og amms like Quickcheck, Ko a o Smallcheck bu pu suing he idea o a much au oma ic p ocess a he same ime ha i is compa ible wi h se e al p og amming languages ( unc ional and non- unc ional ones). To do so ou i s objec i e is o ge id o he obliga ion om he use o de ine a new gene a o o each o he newly de ined da a ypes. Doing so i would be he p og amm i sel he one ha ing o analyze hose ypes and o deduc a gene a o i ing each o hem. In o de o be able o do his second change we c ea ed an In e media e Rep esen a ion (IR) o which all p og amms a e ansla ed be o e being es ed which makes posible o w i e a pla o m independen o all p og amming languages. In his p ojec we will also explain he class s uc u e o CaseGene a o and i ’s code o make clea all he ideas behind i ’s beha iou oge he wi h why we decided o use some echnologies as he lib a y Gene ics o he GHC compile and he Haskell ex ension called Templa e Haskell. Finally a e explaining how he pla o m wo ks we will show some examples abou he p og am beha iou while execu ed wi h eal unc ions. 1.3 Palab as cla e p ueba, e i icaci´on, au om´a ica, caja neg a, p uebas basadas en ase os 1.4 Keywo ds es ing, e i ica ion, au oma ic, black box, asse ion based es ing 6 Cap´ı ulo 2 P elimina es 2.1 P oyec o CAVI-ART En es a secci´on explicamos el p oyec o CAVI-ART, ac ualmen e en ase de desa ollo en la UCM y del cual o ma pa e mi TFG. La pla a o ma CAVI-ART ( ease el esquema de la igu a 2.1) consis e en un conjun o de he amien as pensadas pa a ayuda al p og amado en la alidaci´on de p og amas esc i os en di e en es lenguajes. Es as ayudas incluyen la ex acci´on au- om´a ica y p ueba de condiciones de e i icaci´on, la p ueba au om´a ica de e minaci´on (siemp e que sea decidible usando la ecnolog´ıa ac ual), la in e encia au om´a ica de algunos in a ian es y la gene aci´on au om´a ica y ejecuci´on de casos de p ueba. [6, 3, 5] Un aspec o cla e de la pla a o ma es su Rep esen aci´on In e media de los p o- g amas (de aqu´ı en adelan e IR). Los p og amas esc i os en lenguajes con encionales como C++, Ja a, Haskell, OCaml y o os, se aducen a la IR, sob e la que se e- alizan odas las ac i idades mencionadas an e io men e. La in enci´on es p og ama la mayo pa e de la pla a o ma una sola ez, de mane a que sea independien e del lenguaje de p og amaci´on u ilizado. La IR se dise˜n´o con la in enci´on de acili a al m´aximo posible las a eas nomb adas con an e io idad, median e un dise˜no simple que cuen a con muy pocas cons ucciones p imi i as. Nunca se pens´o en la IR como c´odigo ejecu able sino como una sin axis abs ac a pa a acili a el an´alisis es ´a ico y la e i icaci´on o mal. Sin emba go en los ´ul imos meses se decidi´o con e i la IR en c´odigo ejecu able, pa a posibili a la ejecuci´on de p uebas y cons ucci´on de he amien as de es eo, ambas independien es del lenguaje. Es o supone una en aja ya que la mayo ´ıa de las he amien as de es eo exis en es es ´an ligadas a un lenguaje en conc e o. La pa e del p oyec o enca gada de aduci la IR a Haskell y hace ejecu ables los ase os se ha ealizado den o del abajo de in de g ado de Ma a A acil Mu˜noz con ´ı ulo Implemen aci´on de ase os ejecu ables pa a una pla a o ma de e i icaci´on que ambi´en se engloba den o del p oyec o CAVI-ART. 7 Figu a 2.1: Esquema del p oyec o CAVI-ART 2.2 QuickCheck Quickcheck [2] es una he amien a de Haskell pensada pa a p oba unciones esc i as en dicho lenguaje sob e un conjun o de casos de p ueba gene ados de mane a alea o- ia. Dicho p og ama esul ´o se de g an ayuda, pues iene ideas simila es a lo que que ´ıamos consegui con nues o p oyec o, ya que se a a ambi´en de un sis ema de p ueba ipo caja neg a. Sin emba go p esen a algunas di e encias, sob e odo en la gene aci´on de los casos de p ueba, ya que Quickcheck los gene a de mane a alea o ia, mien as que nues o p oyec o los gene a ´a, como e emos, de mane a exhaus i a. 2.2.1 Ejemplo de uncionamien o del p og ama En es e caso amos a abaja con la siguien e p opiedad de las lis as, cie a pa a cualquie lis a ini a. p op_Re App xs ys = e e se (xs++ys) == e e se ys++ e e se xs Aho a lanzamos el p og ama Quickcheck pa a comp oba si supe a odos los casos de p ueba. 8 Main>QuickCheck p op Re App OK: passed 100 e s s . Veamos aho a que pasa en caso de que nues a unci´on no es ´e de inida co ec a- men e. p op_Re App2 xs ys = e e se (xs++ys) == e e se xs++ e e se ys Al ejecu a la nue a uncion desde Quickcheck. Main> quickcheck p op_Re App2 Falsi iable, a e 1 es s: [2] [-2,1] Aqu´ı podemos obse a que en caso de allo Quickcheck nos de uel e el con ae- jemplo de ama˜no m´ınimo, lo que nos indica es a ez es que nues a de inici´on ha allado en el p ime es y que en dicho caso las espec i as lis as pa a las que ha sido p obado also son [2] y [-2,1]. 2.2.2 Leyes condicionales En algunos casos las leyes que que emos de ini no pueden se ep esen adas median e una simple unci´on y solo son cie as bajo unas p econdiciones muy conc e as. Pa a dichos casos Quickcheck cuen a con el ope ado de implicaci´on ==> pa a ep esen a dichas leyes condicionales. Po ejemplo una ley an simple como la siguien e: x<= y ==>max x y == y Puede se ep esen ada median e la siguien e de inici´on. p op_MaxLe :: In -> In -> P ope y p op_MaxLe x y = x <= y ==> max x y == y En es e ejemplo podemos obse a que el esul ado de la unci´on es de ipo P ope y en ez de Boolean, lo cual es debido a que en el caso de las leyes condi- cionales en ez de p oba la p opiedad pa a 100 casos alea o ios, ´es a es p obada con a 100 casos que cumplan la p econdici´on es ablecida. Si uno de los candida os no la cumple se ´a desca ado y se conside a ´a el siguien e. Quickcheck gene a un m´aximo de 1000 casos de p ueba y si en e ellos no se han encon ado al menos 100 que cumplan la p econdici´on, simplemen e in o ma al usua io cuan os la cumplen. Dicho l´ımi e es ´a pensado pa a que en caso de que no exis an m´as casos que cumplan dicha p econdici´on el p og ama no busque inde inidamen e. 9 16 Cap´ı ulo 3 Nues a p opues a: las clases All , Sized y A bi a y 3.1 Black box es ing en nues o con ex o En el mundo del es ing exis en dos g andes posibilidades: sis emas de ipo caja neg a y sis emas de ipo caja blanca. Los de caja neg a son aquellos sis emas de es ing que no se basan en la es uc u a in e na, si no que abajan ´unicamen e con la en ada, sob e la que aplican una p econdici´on, y la salida sob e la que comp ueban si cumple las pos condiciones es ablecidas. En cambio los de caja blanca no es ean ´unicamen e las en adas y salidas del p og ama aplicandoles p econdiciones y comp obando la pos condiciones, sino que adem´as se basan en la es uc u a in e na del p og ama pa a ealiza la gene aci´on de casos de p ueba, de o ma que se cub a odo el ex o del p og ama. Seg´un el c i e io de cobe u a deseado se pueden gene a casos pa a eje ci a odas las condiciones o odas las amas o odos los caminos. En el caso de nues o p oyec o nos decidimos po el m´e odo de caja neg a, pues que ´ıamos consegui un sis ema ´alido pa a pode p oba cualquie p og ama sin necesidad de ene que ol e a gene a los casos de p ueba cuando cambia la es- uc u a in e na del p og ama. Esa es una de las des en ajas del es eo de ipo caja blanca, que pa a pode comp oba pa es de la es uc u a in e na de un p og ama end ´ıamos que adap a la pla a o ma pa a cada uno de los nue os p og amas. La idea p incipal de ´as de nues o p oyec o e a p incipalmen e la inmedia ez y la comodidad del usua io, es deci que pa a p oba un p og ama no ue a necesa io esc ibi c´odigo ex a, apa e del ya exis en e p og ama, sino que solo ue a especi ica como quie e que se gene en los casos de p ueba y los angos de los dominios a usa y con eso sea ya capaz de p oba su p og ama, lo cual se ajus a mucho m´as a la idea de es eo de caja neg a. Las posibles mane as en las que el usua io puede especi ica como se gene an los casos de p ueba pa a cada a gumen o son 3: •Gene a ncasos de p ueba de mane a alea o ia. 17 •Coge ncasos de p ueba de ama˜no meno o igual a m. •Coge los np ime os casos de p ueba de la lis a de odos los alo es, sea cual sea su ama˜no. 3.2 Sized En la es uc u a del p oyec o, Sized es ´a pensada como la clase ex e na que he eda de All (la cual se puede e en la igu a 3.1). A su ez es la clase que se ocupa de de ol e la lis a de los casos de p ueba a pa i de la lis a all de odos los alo es de un ipo de da os. Es o se ealiza median e dos unciones: •sized que de uel e los np ime os casos meno es o iguales a un ama˜no m. •smalles que de uel e los np ime os casos de la lis a all seg´un su posici´on y sin impo a su ama˜no. En es a clase del p oyec o decidimos implemen a el concep o de ama˜no de un elemen o median e la lib e ´ıa Gene ics explicada an e io men e, pues de esa mane a pod ´ıamos ene una ep esen aci´on del ama˜no independien e del ipo y no hay que de ini lo pa a cada ipo nue o c eado po el usua io. En p ime luga debemos de ini la clase ex e na de la pa e de Gene ics que se ´a la que noso os usemos. En ella, s´olo debemos de ini las unciones que que emos que enga y como se comunica con la clases in e nas de Gene ics. P ime o de inimos la uncion en si, que dada un elemen o de un ipo cualquie a nos de uel a un en e o que ep esen a ´a su ama˜no. Despu´es debemos de ini como se comunica la unci´on size ex e na con la e si´on gen´e ica gsize pa a ob ene de es a el alo a de ol e . En es e caso usamos la unci´on om ecibe un alo en su ep esen aci´on no gen´e ica y lo ans o ma a su ep esen aci´on gen´e ica pa a que pueda se manipulado en las di e en es unciones. En es e caso es simple pues el alo del ama˜no ob enido po gsize se ´a el mismo de uel o po nues a unci´on size. Finalmen e c eamos la clase in e na GSized y de inimos la unci´on gsize. Una ez enemos la in e az en e las dos clases Sized yGSized lo siguien e que debemos de ini es el cons uc o sin a gumen os, que en nues o caso de uel e el ama˜no 0. A con inuacion de inimos size pa a un ipo compues o po o os dos, el ama˜no de dicho ipo es la suma de los ama˜nos de los ipos que los componen. T as ello de inimos el compo amien o cuando el ipo iene mas de un cons uc o posible, en es e caso si elegimos el cons uc o de la de echa el ama˜no del ipo se ´a el del ipo de la de echa y simila si elegimos el cons uc o de la izquie da. Po ´ul imo, enemos la ins ancia u ilizada pa a abaja con la me ain o maci´on del ipo, que en nues o caso al no se necesa ia dicha in o maci´on simplemen e llamamos de nue o a la uncion gsize igno ando la me ain o maci´on. 18 Figu a 3.1: Clase Sized 3.3 All /Templa eAll En p ime luga amos a a a la clase All , cuyas ins ancias cuen an unicamen e con una unci´on, all la cual de uel e la lis a de odos los posibles alo es del ipo de da os en o den c ecien e de amaos. Al p incipio es a clase es aba pensada pa a se una ´unica clase que u iliza a la lib e ´ıa Gene ics y pa a con a con un m´e odo, compose (su uncin se explica ms adelan e) con el cual se capaces de gene a ins ancias de la clase All pa a los ipos de inidos po el usua io. Dicha unci´on se enca ga ´ıa de c ea la lis a de odos los alo es (all ) pa a el nue o ipo de da os a pa i de las lis as de los ipos p ede inidos, pe o a la ho a de in eg a lo con la clase Sized encon amos un p oblema. La idea que en´ıamos sob e es a clase e a da le al usua io la posibilidad de pedi los n alo es mas 19 peque˜nos de una clase o los np ime os alo es de ama˜no meno o igual a un n´ume o p e ijado po ´el. Lo cual en aba en con lic o con la mane a en la que gene ´abamos las lis as de all pa a los ipos de inidos po el usua io. Dadas dos lis as la idea es ealiza el p oduc o ca esiano de ellas siendo es e el esul ado de gene a odas las pa ejas con un alo de la p ime a lis a y o o de la segunda. Teniendo en cuen a que ambas pueden se in ini as, dicho p oduc o debe ´a se ealizado po diagonales, mos amos la idea en la igu a 3.2. La combinaci´on de lis as in ini as pod´ıa se ealizada sin p oblemas usando Gene ics, pe o el p oblema llegaba a la ho a de que e de ol e los np ime os alo es de un ama˜no meno o igual am, ya que pa a ello deb´ıamos o dena la lis a in ini a y encon amos el p oblema de que en dichas lis as in ini as el n´ume o de elemen os de un ama˜no dado siemp e es in ini o y que siemp e hay alg´un elemen o m´as de ama˜no meno o igual a m, aunque es despu´es de muchos elemen os in e medios que no lo son. Exis e un segundo p oblema que es el del o den de los cons uc o es, ya que debemos ga an iza que en la unin de dos al e na i as los casos base se gene an an es que los ecu si os. Es os p oblema nos hicie on pensa en u iliza Templa e Haskell en luga de Gene ics. En la e si´on de ini i a del p og ama en el mdulo Templa eAll se encuen a es a uncionalidad de c ea una ins ancia de All pa a los ipos de da os de inidos po el usua io, u ilizando pa a ello gen all , con la ayuda de la ya nomb ada unci´on compose (su cdigo se mues a en la igu a 3.3). La unci´on compose se enca ga de conca ena odas las diagonales en una ´unica lis a inal, que es la que se de uel e median e la unci´on all , po o o lado diags se enca ga de c ea una de las diagonales y mien as no sea la ´ul ima y de ol e a llama se a s´ı misma con los pa ´ame os pa a la siguien e. Los pa ´ame os de la unci´on diags son: •ise a a del o dinal de la diagonal que amos a gene a . •xs eys se a an de las dos lis as que amos a combina . Adem´as, den o de Templa eAll exis en es unciones que se enca gan de c ea una ins ancia adecuada de la clase All pa a cada uno de los ipos de da os de inidos po el usua io. La p ime a de ellas, y la m´as ex e na en dicho p oceso es gen all , la cual adem´as de llama a ypeIn o pa a ex ae la in o maci´on del ipo y pasa sela a las sub un- ciones, es ambi´en en la que se de ine, den o de gen body, como se o ma ´a exac a- men e la nue a unci´on all pa a la ins ancia del ipo. Los es an es de alles sob e gen all pueden e se en el cdigo que se adjun a en el apndice, apa ado 8.3. La siguien e unci´on a a a , gen ins ance 8.3 se enca ga de c ea una ins ancia de la clase All pa a el nue o ipo de da os (pa ´ame o o ype) y adjun a a dicha ins ancia la de inici´on de la unci´on all que se c ea en gen clause. Po ´ul imo enemos la unci´on gen clause que es esponsable de c ea la de inici´on de la unci´on all pa a el ipo de da os, usando pa a ello la unci´on gen body que hab´ıa sido de inida an e io men e en gen all . Adem´as, cuen a con una se ie de unciones auxilia es que ealizan pa e del p ocesamien o: 20 •lis O FOu se enca ga de c ea la lis a de nomb es de a iables en e 1y n pa a aquellos casos en los cuales los cons uc o es ienen m´as de un pa ´ame o. •isRec de uel e una lis a de booleanos en la cual cada posici´on indica si el cons uc o en dicha posici´on es ecu si o o no. • eo de L si e pa a eo dena los cons uc o es (lo cual es equi alen e a las lis as con la in o maci´on po cada cons uc o ) de mane a que queden en p ime luga aquellos que no son ecu si o y al inal los que si lo son. Es o es necesa io, ya que los cons uc o es ecu si os ha ´an uso de aquellos que no lo son y po ello los no ecu si os deben de ini se en p ime luga . •gen whe es que es esponsable de de ini las clausulas whe e necesa ias pa a odos aquellos cons uc o es con m´as de un pa ´ame o que necesi en u iliza una unci´on auxilia (que son las ep esen adas po las ’s). • uplePa am c ea las uplas de pa ´ame os pa a cada una de las unciones aux- ilia es . 3.4 Ins ancias p ede inidas En es e ´ul imo apa ado mos amos las ins ancias den o de las clases Sized yAll pa a los es ipos b´asicos (In ,Cha yBool) y pa a los ipos que se deducen di ec- amen e de ellos, como es el caso de lis as de cualquie ipo ya ins anciado en dichas clases o las uplas de has a longi ud 6. (El cdigo co espondien e a dichas ins ancias se adjun a en el apndice, apa ado 8.1) Como podemos obse a en el caso de la ins ancia en la clase Sized, cualquie elemen o de uno de los es ipos end ´a ama˜no uno. En el caso de las ins ancias de los es ipos en la clase All , simplemen e debemos indica el conjun o de alo es de dicha clase que se ´an elegibles a la ho a de gene a casos de p ueba, pa a las cuales u ilizamos la unci´on de compose explicada con an e io idad. En el caso de las ins ancias de i adas den o de la clase Sized ´es as se gene an median e Gene ics. 21 Figu a 3.2: Esquema uncionamien o compose 22 Figu a 3.3: Funci´on compose 23 24 Cap´ı ulo 4 El gene ado de casos 4.1 La in e az con la UUT En es e cap´ı ulo amos a a a las di e en es ases del p oceso de es eo po las que pasa el p og ama, u ilizando pa a ello un ejemplo de uncionamien o, en es e caso una unci´on inse en una lis a o denada. En p ime luga amos a echa un ojo a la Uni Unde Tes ing (a pa i de aho a UUT) que se a a de la clase que con iene oda la in o maci´on sob e la unci´on que amos a es ea en cada momen o. Podemos obse a la o ma que iene en la igu a 4.1. Es e a chi o Haskell en el caso de nues o p og ama es sin e izado a pa i de la unci´on p opo cionada po el usua io u ilizando la he amien a IR2Haskell men- cionada en la secci´on 2.1 y podemos obse a que incluye: •uu Name indica el nomb e de la unci´on a es ea pa a e ec os de nomb a la cuando se p esen an los esul ados al usua io •Po ul imo las es unciones uu P ec,uu Me hod yuu Pos acompa˜nadas de las unciones auxilia es necesa ias. En caso de que las unciones u iliza an alg´un ipo de da os de inido po el usua io su de inici´on se inclui ´ıa ambien en el a chi o UUT. 4.2 La ob enci´on del ipo de la UUT El siguien e paso analiza los ipos de los pa ´ame os de en ada de la unci´on que que emos p oba , de esa mane a pod emos gene a casos de p ueba pa a dichos ipos de da os. Nos basa emos pa a e el p oceso en el ejemplo de inse comenzado en el apa ado an e io . Es e p oceso se ealiza median e la unci´on ge inp ypes y sus unciones aux- ilia es, cuyo c´odigo puede encon a se en la p ime a pa e del ap´endice. 25 Figu a 5.1: Casos de la p ime a p ueba que pasa on la p econdici´on 5.3 Inse a un elemen o en un ´a bol Funci´on: inse BST x P econdici´on: P ec(x, ) = so ed(ino de ( )) es deci , la p opiedad de se un ´a bol de b´usqueda Pos condici´on: P os (x, , es) = so ed(ino de ( es))pe mu (x:ino de ( ), ino de ( es)), es deci ambas lis as ienen los mismos elemen os Se gene a on pa a p oba dicha unci´on un o al de 1000 casos de p ueba, de los cuales pasa on la p econdici´on un o al de 518 casos de p ueba. De odos esos casos de p ueba que pasa on la p econdici´on odos ellos pasa on la pos condici´on, no encon amos casos que la con adije an. 5.4 B´usqueda en un ´a bol Funci´on: sea ch x P econdici´on: P ec(x, ) = so ed(ino de ( )) es deci , la p opiedad de se un ´a bol de b´usqueda Pos condici´on: P os (x, , es) = es ↔x∈ino de ( ) es deci , el esul ado es cie o 32 si, y solo si, x pe enece al ´a bol Se gene a on pa a p oba dicha unci´on un o al de 1000 casos de p ueba, de los cuales pasa on la p econdici´on un o al de 518 casos de p ueba. De odos esos casos de p ueba que pasa on la p econdici´on 45 de ellos no pasa on la pos condici´on. 5.5 Conclusiones de los expe imen os En las cua o p uebas podemos obse a que de los 1000 ejemplos gene ados, en odos ellos un po cen aje azonable pasa la p econdici´on, incluso en el segundo caso que es el que cuen a con una p econdici´on m´as ue e. En los es casos en los cuales la de inici´on de la unci´on, su p econdici´on y pos - condici´on son co ec as nues o p og ama no de ec a ningun e o , odos lo casos de p ueba que cumplen la p econdici´on son acep ados como co ec os, en cambio en el ´ul imo de los casos, el cual ue de inido inco ec amen e a p op´osi o el p og ama de- ec a que es ´a de inido inco ec amen e con una buena can idad de con aejemplos, ce ca de un 10% de los casos que pasa on la p econdici´on. 33 34 Cap´ı ulo 6 T abajo elacionado y conclusiones 6.1 Ko a La p ime a de las he amien as que amos a a a en es e apa ado es Ko a [1], una he amien a de Ja a que si e pa a la gene aci´on de casos complejos de p ueba a pa i de unas es icciones dadas. La idea de ´as de Ko a es que dado un p edicado en Ja a y una unci´on ini ializa ion en la cual de inimos los dominios pa a cada una de las clases del inpu , es deci los alo es ´alidos pa a cada una de ellas, explo a el espacio de es ados de las posibles soluciones gene ando s´olo soluciones no-isomo icas en e si, de es a mane a consigue una g an poda de las soluciones no in e esan es del espacio de b´usqueda. Lo p ime o que hace Ko a es ese a el espacio necesa io pa a los obje os es- peci icados, en el caso de un BinT ee ese a ia espacio pa a ´el y pa a el n´ume o de Nodos que que amos. Po ejemplo, si que emos un ´a bol con es nodos el ec o con end ´ıa 8 campos: •2 pa a el BinT ee (uno pa a la a´ız y o o pa a el ama˜no). •2 campos po cada uno de los 3 nodos (hijo izquie do/hijo de echo). Cada uno de los posibles candida os que conside e Ko a a pa i de ese momen o se ´a una e aluaci´on de esos 8 campos. Po lo an o el espacio de es ados de b´usqueda del inpu consis e en odas las posibles combinaciones de esos campos, donde cada uno de ellos oma alo es de su dominio de inido en ini ializa ion. Pa a consegui explo a de mane a sis em´a ica y comple a el espacio de es ados, Ko a o dena odos los elemen os en los dominios de las clases y los dominios de los campos. Dicho o den den o de cada uno de los dominios de los campos se ´a consis en e con el del dominio de la clase y odos los alo es que pe enezcan al mismo dominio de clase ocu i an de mane a consecu i a en el dominio del campo. 35 T as es o, cada candida o de la en ada se esp esen a como un ec o de ´ındices de sus co espondien es dominios de campos. T as de ini los dominios de cada uno de los campos del ec o comienza la busqueda con la inicializaci´on a 0 de odos los indices del ec o . A con inuaci´on ijamos los alo es de los campos pa a cada posible candida o de acue do a los alo es en el ec o y ac o seguido in oca a la uncion epOk que es donde el usua io ha de inido la p econdici´on. Du an e dicha ejecuci´on Ko a moni o iza el o den en que son accedidos los campos del ec o y cons uye una lis a con los iden i icado es de los campos, o denados po la p ime a ez en que epOk los accede. Cuando epOk e o na Ko a gene a el siguien e candida o inc emen ando el ´ındice del dominio de campo pa a el campo que se encuen a ´ul imo en la lis a o de- nada cons uida p e iamen e. Si dicho ´ındice es mayo que el ama˜no del dominio de su campo, es e se pone a ce o y se inc emen a el ´ındice de la posici´on an e io y as´ı sucesi amen e. Al segui es e m´e odo pa a gene a el siguien e candida o consegui e- mos poda un g an n´ume o de ellos que ienen la misma e aluaci´on pa cial sin deja ue a ninguno ´alido. El algo i mo de busqueda desc i o aqu´ı gene a las en adas en o den lexicog ´a ico. Adem´as, pa a los casos en los que epOk no es de e minis a, es e m´e odo ga an iza que son gene ados odos los candida os pa a los que epOk de uel e T ue. Los casos pa a los que siemp e de uel e False nunca son gene ados y los casos pa a los que alguna ez se de uel e T ue y o as eces False pueden se gene ados o no. Dos candida os se ´an de inidos como isomo os si las pa es de sus g a os alcanz- ables desde la a´ız son isomo as. En el caso de epOk el obje o a´ız es aquel pasado como a gumen o impl´ıci o. El isomo ismo en e candida os di ide el espacio de es ados en pa iciones isom´o icas (debido al o denamien o lexicog ´a ico in oducido po el o den de los alo es de los dominios de los campos y la o denaci´on de los campos ealizado po epOk). Pa a cada una de dichas pa iciones isomomo icas Ko a gene a ´unicamen e el candida o lexicog ´a icamen e meno . Adem´as, con el p oceso explicado an e io men e pa a gene a el siguien e can- dida o, eniendo en cuen a la lis a de o denaci´on de los campos, Ko a se asegu a de no gene a a ios candida os den o de la misma pa ici´on isom´o ica. 6.2 Smallcheck La segunda he amien a a a a en es e apa ado es Smallcheck [7] una lib e ´ıa pa a Haskell usada en el es ing basado en p opiedades. Es a lib e ´ıa pa e de las ideas del Quickcheck y pe ecciona algunos de los pun os lacos de es e. La p incipal di e encia de Smallcheck espec o a Quickcheck es la o ma en que gene a sus casos de p ueba. En es e caso Smallcheck se apoya en la ”hip´o esis del ´ambi o peque˜no” la cual dice que si un p og ama no cumple su especi icaci´on en alguno de sus casos casi siemp e exis i ´a un caso simple en el cual no la cumpla o lo que iene a se lo mismo, que si un p og ama no alla en casos peque˜nos lo no mal es que no alle en ninguno de sus casos. 36 Pa iendo de es a idea cambia la gene aci´on exis en e en Quickcheck, que e a alea o ia, po una gene aci´on exhaus i a de odos los casos de p ueba peque˜nos, o - denados po p o undidad (que es el nomb e usado pa a el ama˜no), dejando a c i e io del usua io has a que p o undidad deben conside a se como peque˜nos. A con inuaci´on p esen a emos como es ´an de inidas las p o undidades m´as impo an es: •En el caso de los ipos de da os algeb aicos, como es usual, la p o undidad de una cons ucci´on de a idad ce o es ce o mien as que la p o undidad de una cons ucci´on de a idad posi i a es una m´as que la mayo de odos sus a gumen os. •En el caso de las uplas, dicha p o undidad se de ine de mane a un poco di e - en e. La p o undidad de una upla de a idad ce o es ce o pe o la de una upla de a idad posi i a es la mayo p o undidad de en e odas las de sus componen es. •En el caso de los ipos num´e icos, la de inici´on de la p o undidad se ealiza con espec o a una ep esen aci´on imagina ia como una es uc u a de da os. De es a mane a, la p o undidad de un en e o ise ´a su alo absolu o, ya que se cons uy´o de mane a algeb aica como SucciZe o. A su ez, la p o undidad de un nume o decimal sx2ees la de la upla de en e os (s,e). Smallcheck de ine una clase Se ial de ipos que pueden se enume ados has a una de e minada p o undidad. Exis en ins ancias p ede inidas de la clase Se ial pa a odos los ipos de da os del p eludio . Sin emba go, es muy ´acil de ini una nue a ins ancia de dicha clase pa a un ipo de da os algeb aico, ´es a es de un conjun o de combinado es cons<N>, gen´e icos pa a cualquie combinaci´on de ipos Se ial, donde Nes la a idad del cons uc o . Supongamos un ipo de da os en Haskell P op en el que enemos una a iable, la negaci´on de una a iable y el O de dos a iables. da a P op = Va Name |No P op |O P op P op Pa a dicho ipo de da os de ini una ins ancia de la clase Se ial, asumiendo una de inici´on simila pa a el ipo Name, se ´ıa. in s a nce S e i a l P op whe e s e i e s = cons1 Va / cons1 No / cons2 O Una se ie es simplemen e una unci´on que dado un en e o de uel e una lis a ini a. ype S e i e s a = In −>[a] A su ez el p oduc o y la suma sob e dos se ies se de inen como: ( /) : : S e i e s a −>Se ies a −>Se ies a s1 / s2 = d−>s1 d ++ s2 d (><) : : S e i e s a −>Se ies b −>S e i e s ( a , b) s1 >< s2 = d−>[ ( x , y ) |x<−s1 d , y <−s2 d ] 37 Po ´ul imo, los combinado es cons<N> es ´an de inidos usando >< dec emen ando y comp obando la p o undidad co ec amen e. cons0 c = d−>[c] cons1 c = d−>[ c a |d>0 , a <−se ies (d−1)] cons2 c = d−>[ c a b |d>0 , (a , b) <−(se ies >< se ies) (d−1)] Cuando se usa muchas eces el esquema gene al pa a de ini alo es de p ueba se p oduce que pa a alguna p o undidad peque˜na dlos 10.000-100.000 casos de p ueba son comp obados ´apidamen e, pe o pa a la p o undidad d+1 esul e imposible com- ple a los miles de millones de casos de p ueba. Po ello, esul a necesa io educi algunas dimensiones del espacio de b´usqueda de mane a que o as de las dimensiones puedan se comp obadas en mayo p o undidad. El p ime pun o a ene en cuen a es, que a pesa de que los n´ume os en e os pueden pa ece una elecci´on ob ia como alo es base pa a las p uebas, debemos con- side a que los espacios de busqueda pa a los ipos compues os (especialmen e un- cionales) al usa bases num´e icas, c ecen de mane a muy ´apida. En muchos casos el ipo booleano puede se una elecci´on pe ec amen e ´alida pa a los alo es base, y con ello se consegui ´oa educi en g an medida el espacio de busqueda espec o a la u ilizaci´on de en e os. Exis e o a e si´on de Smallcheck llamada Lazy Smallcheck, que a su ez se ap o echa de la e aluaci´on pe ezosa de Haskell, la cual pe mi e que una unci´on de- uel a un alo , aunque es a es ´e aplicada sob e una en ada de inida pa cialmen e. Es a posibilidad de ob ene el esul ado de una unci´on sob e muchas en adas en una sola ejecuci´on, puede esul a de g an ayuda en el es eo basado en p opiedades, ya que si una unci´on se cumple pa a una soluci´on pa cial, es a se cumpli ´a pa a odas las unciones o almen e de inidas que pa an de la misma. En eso se cen a el Lazy Smallcheck, en e i a gene a odas esas unciones o almen e de inidas que no apo - an nada de in o maci´on ex a sob e la de inici´on pa cial. La ac ual e si´on de Lazy Smallcheck es capaz de es ea p opiedades de p ime o den con o sin cuan i icado es uni e sales. 38 Cap´ı ulo 7 Conclusiones del p oyec o 7.1 Conclusiones La idea de gene a alo es pa a ipos de da os p ede inidos y de inidos po el usua io median e el uso de las clases de Haskell ya es ´a p esen e an o de Quickcheck como en Smallcheck. La idea de gene a casos de p ueba exhaus i os has a un cie o ama˜no, ambi´en es ´a p esen e an o en Smallcheck como en Ko a . La di e encia p incipal de nues o abajo con es os es que los es equie en que el usua io esc iba c´odigo adicional pa a los ipos del usua io que son desconocidos pa a el sis ema. En el caso de Quickcheck, hay que gene a manualmen e la ins ancia de la clase A bi a y, si bien el sis ema o ece una se ie de combinado es que acili an la a ea. En el caso de Smallcheck, hay que esc ibi manualmen e una ins ancia de la clase Se ial, y en el caso de Ko a hay que edi a una plan illa pa a de ini una noci´on de ama˜no y pa a e i a gene a alo es duplicados. En nues o abajo, an o la noci´on de ama˜no, como las ins ancias de la clases All y Sized, se gene an au om´a icamen e pa a los ipos desconocidos, g acias al uso de espec i amen e Templa e Haskell y Gene ics. Ello unido a que el c´odigo de la p econdicion y la pos condici´on son gene ados au om´a icamen e po la he amien a p e ia IR2Haskell, hace que oda el p oceso de p ueba desde que el usua io esc ibe su c´odigo y ase os o iginales, has a que se ejecu an las p uebas y se de ec an los posibles e o es, se haga sin ninguna in e enci´on manual. Du an e la c eaci´on de los expe imen os epo ados en es e abajo, la he amien a ue capaz de de ec a e o es no in encionados, an o en las pos condiciones inicial- men e esc i as, como en el c´odigo bajo p ueba, lo cual a la ez si i´o pa a asegu a nos de que la he amien a de ec a de mane a co ec a e o es en la de inici´on de la unci´on. 7.2 Conclusions The idea o gene a ing alues bo h o he p ede ined da a ypes and he ypes de- ined by he use using Haskell classes is al eady p esen bo h in Quickcheck and 39 Smallcheck. The idea abou gen a ing exhaus i e es cases o a ce ain size is also p esen bo h in Smallcheck and Ko a . The main di e ence be ween ou p ojec and all hose p ojec s a e ha hose h ee need he use o w i e addi ional code o he use -de ined da a ypes ha a e no know by he sys em. In Quickcheck is necessa y o manually gene a e ins ance o he A bi a y class using a se o combine s gi en o do so. In he case o Smallcheck i ’s necessa y o manually c ea e an ins ance o he Se ial class and in Ko a you ha e o edi a empla e o de ine he concep o size and being able o a oid duplica ed alues. In ou p ojec , bo h he concep o size and he ins ances o All and Sized classes a e au oma ically gene a ed o all he unknown da a ypes hanks o Templa e Haskell and Gene ics. This oge he wi h he ac ha he code o he p econ- di ion and pos condi ion a e au oma ically gene a ed by he ool IR2Haskell makes all he es ing p ocess, om he momen in which he use w i es i s code and asse s un il he momen in which es s a e execu ed and he possible e o s a e de ec ed low wi hou any in e en ion om he use . Du ing he c ea ion o he expe imen s shown in his p ojec , he ool was able o ind some non in ended e o s bo h in some i s ly w i en pos condi ions and code unde es , which se ed us o be comple ely su e abou he co ec unc ioning o he ool as i was able o de ec inco ec ness in he unc ion de ini ion 40 Cap´ı ulo 8 Ap´endice 8.1 Ins ancias p ede inidas -- | Fo basic ypes we mus gi e he ins ances ins ance Sized In whe e size x = 1 ins ance All In whe e all = [1..5] ins ance Sized Cha whe e size x = 1 ins ance All Cha whe e all = [’a’..’z’] ins ance Sized Bool whe e size x = 1 ins ance All Bool whe e all = [T ue, False] ins ance Sized a => Sized [a] ins ance (Sized a, Sized b) => Sized (a,b) ins ance (Sized a, Sized b, Sized c) => Sized (a,b,c) ins ance (Sized a, Sized b, Sized c, Sized d) => Sized (a,b,c,d) ins ance (Sized a, Sized b, Sized c, Sized d, Sized e) => Sized (a,b,c,d,e) 41 8.5 UUTs de los di e en es casos de p ueba 8.5.1 Inse a en una lis a o denada module UUT whe e impo quali ied A ays as A impo quali ied Bags as B impo quali ied Se s as S impo quali ied Sequences as Q impo Asse ion impo Da a.Lis uu Na gs :: In uu Na gs = 2 uu Me hods :: [S ing] uu Me hods = ["uu P ec", "uu Me hod", "uu Pos "] uu Name :: S ing uu Name = "inse " uu P ec :: In -> [In ] -> Bool uu P ec x xs = so ed xs so ed [] = T ue so ed [x] = T ue so ed (x:y:xs) = x <= y && so ed (y:xs) uu Me hod :: In -> [In ] -> [In ] uu Me hod x [] = [x] uu Me hod x (y:ys) | x <= y = x:y:ys | o he wise = y : uu Me hod x ys uu Pos :: In -> [In ] -> [In ] -> Bool uu Pos x xs ys = ys == so (x:xs) 8.5.2 Inse a en un A ay module UUT whe e impo quali ied A ays as A impo quali ied Bags as B impo quali ied Se s as S impo quali ied Sequences as Q impo Asse ion 48 impo Da a.Lis uu Na gs :: In uu Na gs = 3 uu Me hods :: [S ing] uu Me hods = ["uu P ec", "uu Me hod", "uu Pos "] uu Name :: S ing uu Name = "inse " --TODO usa al p incipio del ou pu uu P ec x m a = e alA $ And (FTe m (Aplic (Aplic (TVa (<=)) ((TCons 0))) ((TVa m)))) (And (FTe m (Aplic (Aplic (TVa (<)) ((TVa m))) (Aplic ((TVa A.len)) ((TVa a))))) (Fo all (Gua dIn Tuple (Tuple2 ((TCons 0)) ((TCons 0))) (Tuple2 (Aplic (Aplic (TVa (-)) (TVa m)) (TCons 1)) (Aplic (Aplic (TVa (-)) (TVa m)) (TCons 1)))) ( (i, j) -> (Imp (FTe m (Aplic (Aplic (TVa (<=)) ((TCons 0))) ((TVa i)))) (Imp (FTe m (Aplic (Aplic (TVa (<=)) ((TVa i))) ((TVa j)))) (Imp (FTe m (Aplic (Aplic (TVa (<)) ((TVa j))) ((TVa m)))) (FTe m (Aplic 49 (Aplic (TVa (<=)) (Aplic (Aplic ((TVa A.ge )) ((TVa a))) ((TVa i)))) (Aplic (Aplic ((TVa A.ge )) ((TVa a))) ((TVa j))))))))))) uu Me hod x m a = le i = (-) m 1 in 2xmia whe e 2xmia= le b1 = (>=) i 0 in case b1 o False -> 4 x m i a T ue -> le e = A.ge a i in le b2 = (<) x e in case b2 o T ue -> le e = A.ge a i in le i2 = (+) i 1 in le ap = A.se a i2 e in le i3 = (-) i 1 in 2 x m i3 ap False -> 4 x m i a 4xmia= le i2 = (+) i 1 in le ap = A.se a i2 x in ap uu Pos x m a es = e alA $ Fo all (Gua dIn Tuple (Tuple2 ((TCons 0)) ((TCons 0))) (Tuple2 ((TVa m)) ((TVa m)))) ( (i, j) -> (Imp (FTe m (Aplic (Aplic (TVa (<=)) ((TCons 0))) ((TVa i)))) (Imp (FTe m (Aplic (Aplic (TVa (<=)) ((TVa i))) 50 ((TVa j)))) (Imp (FTe m (Aplic (Aplic (TVa (<=)) ((TVa j))) ((TVa m)))) (FTe m (Aplic (Aplic (TVa (<=)) (Aplic (Aplic ((TVa A.ge )) ((TVa es))) ((TVa i)))) (Aplic (Aplic ((TVa A.ge )) ((TVa es))) ((TVa j))))))))) 8.5.3 Inse a en un ´a bol -- This ile has been gene a ed by he CAVI-ART CLIR- o-Haskell ans o me ool -# LANGUAGE De i eGene ic #- module UUT whe e impo quali ied A ays as A impo quali ied Bags as B impo quali ied Se s as S impo quali ied Sequences as Q impo Asse ion impo Da a.Lis impo GHC.Gene ics -- Inse ing in a Bina y Sea ch ee -- This is an example whe e he use de ines a new ype da a T ee a = Emp y | Node (T ee a) a (T ee a) de i ing (Gene ic,Show,Eq) uu Na gs :: In uu Na gs = 2 uu Me hods :: [S ing] uu Me hods = ["uu P ec", "uu Me hod", "uu Pos "] uu Name :: S ing 51 uu Name = "inse BST" uu P ec :: In -> T ee In -> Bool uu P ec x = so ed $ ino de ino de Emp y = [] ino de (Node l x ) = ino de l ++ (x : ino de ) so ed [] = T ue so ed [x] = T ue so ed (x:y:xs) = x <= y && so ed (y:xs) uu Me hod :: O d a => a -> T ee a -> T ee a uu Me hod x Emp y = Node Emp y x Emp y uu Me hod x @(Node l y ) | x < y = Node (uu Me hod x l) y |x==y= | x > y = Node l x (uu Me hod x ) uu Pos x o = i x ‘elem‘ ino de hen == o else ino de o == so (x : ino de ) 8.5.4 B´usqueda en un ´a bol -# LANGUAGE De i eGene ic #- module UUT whe e impo quali ied A ays as A impo quali ied Bags as B impo quali ied Se s as S impo quali ied Sequences as Q impo Asse ion impo GHC.Gene ics -- Sea ching in a Bina y Sea ch ee -- This is an example whe e he use de ines a new ype da a T ee a = Node (T ee a) a (T ee a) | Emp y de i ing (Gene ic,Show) uu Na gs :: In 52 uu Na gs = 2 uu Me hods :: [S ing] uu Me hods = ["uu P ec", "uu Me hod", "uu Pos "] uu Name :: S ing uu Name = "sea chBST" uu P ec :: In -> T ee In -> Bool uu P ec x = so ed $ ino de ino de Emp y = [] ino de (Node l x ) = ino de l ++ (x : ino de ) so ed [] = T ue so ed [x] = T ue so ed (x:y:xs) = x <= y && so ed (y:xs) uu Me hod :: O d a => a -> T ee a -> Bool uu Me hod x Emp y = False uu Me hod x @(Node l y ) | x < y = uu Me hod x -- e o , debe ´ıa se l | x == y = T ue | x > y = uu Me hod x uu Pos x o = o == (x ‘elem‘ ino de ) 53 54 Bibliog a ´ıa [1] Chand asekha Boyapa i, Sa az Khu shid & Da ko Ma ino (2002): Ko a : Au oma ed Tes ing Based on Ja a P edica es. A ailable a h p://web.eecs.umich.edu/ bchand a/publica ions/iss a02.pd . [2] Koen Claessen & AJohn Hughes (2000): QuickCheck:A Ligh weigh Tool o Random Tes ing o Haskell P og ams. A ailable a h ps://www.eecs.no hwes e n.edu/ obby/cou ses/395-495-2009- all/quick.pd . [3] Mo eno Falaschi, edi o (2015): Logic-Based P og am Syn hesis and T ans- o ma ion - 25 h In e na ional Symposium, LOPSTR 2015, Siena, I aly, July 13-15, 2015. Re ised Selec ed Pape s.Lec u e No es in Compu e Science 9527, Sp inge , doi:10.1007/978-3-319-27436-2. A ailable a h p://dx.doi.o g/10.1007/978-3-319-27436-2. [4] Magalhaes, A ze Dijks a, Johan Jeu ing & And es Lh (2010): A Gene ic De i ing Mechanism o Haskell. A ailable a h p://www.d eixel.ne / esea ch/pd /gdmh nocolo .pd . [5] Manuel Mon eneg o, Susana Nie a, Rica do Pe˜na & Cla a Segu a (2016): Ex end- ing Liquid Types o A ays. In: PROLE 2016, Salamanca, Spain, pp. 1–15. [6] Manuel Mon eneg o, Rica do Pe˜na & Jaime S´anchez-He n´andez (2015): A Gene ic In e media e Rep esen a ion o Ve i ica ion Condi ion Gene a ion. In: Logic-Based P og am Syn hesis and T ans o ma ion - 25 h In e na ional Sympo- sium, LOPSTR 2015, Siena, I aly, July 13-15, 2015. Re ised Selec ed Pape s, pp. 227–243. [7] Colin Runciman, Ma hew Naylo & F ed ik Lindblad (2008): SmallCheck and Lazy SmallCheck au oma ic exhaus i e es ing o small alues. A ailable a h ps://pd s.seman icschola .o g/2460/c9b40ea3c4bbae 53c5 4ad2717154c 15b5.pd . [8] Tim Shea d & Simon Pey on Jones (2002): Tem- pla e Me a-p og amming o Haskell. A ailable a h ps://www.mic oso .com/en-us/ esea ch/wp-con en /uploads/2016/02/me a-haskell.pd . 55