scieee Science in your language
[es] (orig)

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

Abstract

Una de las partes más 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 últimos años han sido desarrolladas diversas herramientas para automatizar de manera parcial dicho proceso de testeo. Sin embargo la mayoría de ellas están especializadas en un único lenguaje de programación. Nuestro objetivo es conseguir una plataforma que permita el testeo de aplicaciones de manera automática para el usuario y que admita como entrada un programa escrito en cualquier lenguaje de programación. 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ándolos a las necesidades de cada ejecución. 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ás automático, y a la vez compatible con diversos lenguajes de programación tanto funcionales como no funcionales. Para lograr el primer objetivo hemos eliminado la obligación de que el usuario defina un nuevo generador para cada uno de los nuevos tipos definidos. Así, será 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ón Intermedia (IR) a la que se traducen los programas antes de ser testeados y que permite escribir una plataforma independiente del lenguaje de programación. A su vez profundizaremos en la estructura de clases de CaseGenerator y explicaremos su código, de manera que queden claras todas las ideas detrás 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ón de Haskell llamada Template Haskell. Por _ultimo, tras explicar el funcionamiento de la herramienta expondremos algunos ejemplos prácticos del funcionamiento del programa al ser ejecutado con funciones reales.

Read accessible full text

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

Author: García Castillo, Pedro
Year: 2017
Source: https://docta.ucm.es/bitstreams/e226b93b-2a8c-42ce-98b6-611e6c925945/download
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