Uni e sidad Complu ense de Mad id
Facul ad de In o m´a ica
Depa amen o de Sis emas In o m´a icos y Compu aci´on
GENERACI ´
ON DE CASOS DE PRUEBA TIPO
CAJA NEGRA MEDIANTE RESTRICCIONES
T abajo de Fin de G ado
Doble G ado en Ingenie ´ıa In o m´a ica y Ma em´a icas
Junio 2018
Au o :
Miguel Ga ido Canalejas
Di ec o :
Rica do Pe˜na Ma ´ı
ii
Miguel Ga ido Canalejas
Resumen
La pla a o ma de alidaci´on CAVI-ART nos o ece una ep esen aci´on in-
e media de cualquie unci´on esc i a en di e en es lenguajes de p og amaci´on, que
incluye su c´odigo, su p econdici´on y su pos condici´on. Sob e dicha unci´on deseamos
ealiza p uebas de ejecuci´on.
El obje i o de es e abajo eside en c ea de mane a au om´a ica di e en es
casos de p ueba que cumplan las p econdiciones de las unciones que se quie an
p oba . Pa a ello, se han es udiado p ime o los esolu o es SMT, en conc e o Z3, se
han p og amado en al esolu o odas las unciones y ipos que pueden in e esa nos
pa a las p econdiciones, y po ´ul imo se ha c eado, en Haskell, un gene ado de
es icciones que analice las p econdiciones de un p og ama en la IR, g acias a su
ep esen aci´on en o ma de ´a bol abs ac o, y gene e un a chi o de es icciones
p ocesable po Z3 con el que ob ene los casos de p ueba.
Palab as cla e
P uebas de ejecuci´on, esolu o es SMT, gene ado de es icciones, esolu-
ci´on de es icciones, es uc u as de da os.
iii
i
Miguel Ga ido Canalejas
Abs ac
The alida ion pla o m CAVI-ART o e s us an in e media e ep esen a-
ion o any unc ion w i en in di e en languages, including i s p econdi ion, i s
code and i s pos condi ion. We wan o do es ing o hose unc ions.
The goal o his wo k consis s o au oma ically c ea ing di e en es cases
sa is ying he p econdi ions o he unc ions wan ed o be es ed. In o de o do
his, SMT sol e s ha e been s udied, speci ically Z3, e e y unc ion and da a ype
we could be in e es ed in o he p econdi ions ha e been p og ammed, and, inally,
a cons ain s gene a o has been c ea ed in Haskell. I analyzes he p econdi ions o
an IR p og am, hanks o i s abs ac syn ax ee ep esen a ion, and gene a es a
cons ain s ile p ocessable by Z3 om which we ob ain he es cases.
Keywo ds
Tes ing, SMT sol e s, cons ain s gene a o , cons ain s sol ing, da a s uc-
u es.

i
Miguel Ga ido Canalejas
´
Indice gene al
1. In oducci´on 1
2. P elimina es 7
2.1. P oyec oCAVI-ART ........................... 7
2.2. Sis ema ac ual de gene aci´on de casos de p ueba . . . . . . . . . . . . 7
2.3. Lahe amien aZ3 ............................ 9
3. El lenguaje de ase os 15
3.1. Sin axisb´asica .............................. 15
3.2. TipoLis a................................. 16
3.3. TipoA ay ................................ 19
3.4. Tipo ´
A bolBina io............................ 23
3.5. Tipo ´
A bolAVL ............................. 29
3.6. Tipo ´
A bolRojineg o........................... 34
3.7. Doble uso de los p edicados . . . . . . . . . . . . . . . . . . . . . . . 40
4. Es a egia de gene aci´on de casos 45
4.1. Tipos de es icciones . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
4.1.1. Res icciones de ama˜no . . . . . . . . . . . . . . . . . . . . . 46
4.1.2. Res icciones de es uc u a . . . . . . . . . . . . . . . . . . . . 46
4.1.3. Res icciones de con enido . . . . . . . . . . . . . . . . . . . . 47
4.2. Es a egia ................................. 49
5. Expe imen os 55
5.1. Lis as ................................... 55
5.2. A ays................................... 57
5.3. ´
A bolesBina ios ............................. 59
ii
iii ´
INDICE GENERAL
5.3.1. Mon ´ıculos Zu dos . . . . . . . . . . . . . . . . . . . . . . . . 59
5.3.2. ´
A boles de B´usqueda . . . . . . . . . . . . . . . . . . . . . . . 62
5.4. ´
A bolesAVL ............................... 64
5.5. ´
A bolesRojineg os ............................ 69
6. Conclusiones 77
A. P og ama Haskell 81
A.1.Main.................................... 81
A.2.As 2Sm .................................. 84
B. Resul ados de Ejecuci´on 95
B.1.Fiche oSm ................................ 95
B.2.Fiche oTx ................................ 97
Bibliog a ´ıa 103
Miguel Ga ido Canalejas
Cap´ı ulo 1
In oducci´on
Cas ellano
Te minada la c eaci´on de un cie o p og ama, apa ece la a ea de hace
p uebas de ejecuci´on. Es a a ea consis e en comp oba si el p og ama se compo a
como debe ´ıa, median e la ejecuci´on de una se ie de casos de p ueba, y la compa-
aci´on de los esul ados ob enidos pa a dichos casos con las espec i as espues as
espe adas. No malmen e, especi ica y p epa a manualmen e es os casos de p ueba
esul a an o cos oso como poco iable. Es cos oso po que equie e idea casos que se
ajus en a nues o c´odigo, ealiza nume osas ejecuciones, de e mina cu´al debe se
la espues a co ec a en cada caso y comp oba cada uno de los esul ados. Po o o
lado, la poca iabilidad iene de i ada de no conside a odos los casos necesa ios,
pues, ¿y si los casos elegidos son pocos o demasiado sencillos y dejan caminos sin
explo a ? Lo que c eemos que es ´a uncionando co ec amen e esul a ene e o es
que no hemos de ec ado. Au oma iza odo es e p oceso pa ece en onces de sumo
in e ´es.
Podemos clasi ica las es a egias de p uebas en dos g andes g upos: de caja
neg a y de caja blanca [1]. La p ime a de ellas consis e en la gene aci´on de casos
de p ueba bas´andose exclusi amen e en la especi icaci´on del p og ama, es deci , en
las p econdiciones y pos condiciones, sin impo a el c´odigo de la unci´on. De es e
modo, los casos de p ueba debe ´an e i ica la p econdici´on, y el esul ado ob enido
as la ejecuci´on debe ´a sa is ace la pos condici´on. Po su pa e, las p uebas de caja
blanca ienen en cuen a el c´odigo del p og ama y su obje i o es gene a casos que
ejecu en los di e en es caminos que puede segui la ejecuci´on den o del c´odigo.
Enma cado den o del p oyec o CAVI-ART, explicado m´as adelan e, es e
abajo p e ende au oma iza las p uebas de caja neg a median e la gene aci´on de
casos de p ueba que cumplan las p econdiciones eque idas po las dis in as unciones
del p og ama. Dicho p oyec o es ´a en ocado undamen almen e a la e i icaci´on de
p og amas, y po an o cada unci´on es ´a p o is a de p econdici´on y pos condici´on.
En abajos p e ios sob e es a pla a o ma [2], se ha desa ollado una he amien a
que ans o ma un ase o cualquie a en una unci´on ejecu able, de al o ma que se
1
8 CAP´
ITULO 2. PRELIMINARES
Figu a 2.1: Pla a o ma CAVI-ART
posibles casos de p ueba. T as es o, se il aban seg´un la p econdici´on, desca an-
do as´ı odos aquellos que no la cumplie an y que, po an o, no e an ´alidos pa a
e i ica el p og ama. Es e m´e odo esul a cos oso an o en iempo como en ecu -
sos de memo ia, pues o que es amos gene ando muchos casos pa a luego acaba
desca ando un al o po cen aje de ellos.
El p og ama ac ual de gene aci´on de casos de caja neg a ecibe como en-
ada un p og ama Haskell que se ajus a a la es uc u a de la Figu a 2.3, con dos
unciones booleanas e e en es a la p econdici´on y pos condici´on de la unci´on p in-
cipal. De es e modo, los casos de p ueba deben se alo es pa a los a gumen os de
la unci´on x1: 1, . . . , xn: n, donde i e ie e al ipo de la a iable xi, pues o que
son la en ada de la unci´on p incipal. Ob iamen e, la p econdici´on especi ica ´a una
se ie de es icciones sob e es as a iables de en ada. Po ello, los casos de p ueba
gene ados son los u ilizados en la p econdici´on pa a e si se e i ica o no. En caso
de hace lo, puede conside a se como un caso de p ueba ´alido y, en caso con a io,
es desca ado. Los casos ´alidos se pasan po la unci´on, ob eniendo as´ı un esul ado
inal de la misma. Es e esul ado inal, unido a los alo es de las a iables de en a-
da, son usados en la pos condici´on como a gumen os pa a e si cumplen odos los
equisi os de salida necesa ios.
La a ea m´as complicada de es e sis ema eside en la gene aci´on de alo es
pa a las a iables de en ada de la p econdici´on. Y es que, ales a iables pueden se
Miguel Ga ido Canalejas

2.3. LA HERRAMIENTA Z3 9
a::= c{cons an e }
|x{ a iable }
be ::= a{exp esi´on a ´omica }
| ai{aplicaci´on de unci´on/ope ado p imi i o }
| haii { cons ucci´on de uplas }
|C ai{aplicaci´on de cons uc o }
e::= be {exp esi´on ligada }
|le hxi:: τii=be in e{le secuencial }
|le un de iin e{le ecu si o pa a de inici´on de unciones }
|case ao al i[; →e]{case con ama de aul opcional }
lde ::= de ine {ψ1}de {ψ2} { de inici´on de unci´on con p econdici´on y pos condici´on }
de ::= (xi:: τi) :: yi:: τi=e{de inici´on de unci´on (las a iables de salida ienen nomb e) }
al ::= C xi:: τi→e{ ama del case }
τ::= α{ a iable de ipo }
|T τi{aplicaci´on de un cons uc o de ipo }
Figu a 2.2: Sin axis abs ac a de la IR
p eCD(x1: 1, . . . , xn: n) : Bool
un(x1: 1, . . . , xn: n) :
pos CD(x1: 1, . . . , xn: n, x : ) : Bool
Figu a 2.3: Es uc u a del p og ama Haskell ecibido pa a las p uebas de caja neg a
de ipos simples como en e os o booleanos, pe o ambi´en pueden se de ipos an
complejos como lis as, ´a boles ojineg os, o aquellos que el usua io desee in en a se.
Pa a consegui gene a casos de p ueba de o ma co ec a, es necesa io en onces
in es iga el ipo de cada una de es as a iables, pa a as´ı sabe como asigna les
posibles alo es. Pa a ello, se u iliza la he amien a Templa e Haskell. Tal he a-
mien a p opo ciona la posibilidad de analiza los ipos de cada m´e odo, accediendo
a su de inici´on pa a aquellos que son desconocidos ( ipos algeb aicos de inidos en
el p og ama). De es e modo, una ez se ienen iden i icados cada uno de los ipos,
el p og ama de caja neg a gene a odos los alo es posibles has a un cie o ama˜no
ijado po el usua io pa a cada uno de ellos, log ando as´ı odas las asignaciones po-
sibles pa a las a iables que i ´an pas´andose po la p econdici´on, unci´on p incipal y
pos condici´on.
2.3. La he amien a Z3
El p oblema de la sa is ac ibilidad m´odulo eo ´ıas (SMT del ´e mino Sa-
is iabili y Modulo Theo ies en ingl´es), es un p oblema de decisi´on pa a ´o mulas
l´ogicas de p ime o den, con espec o a cie as eo ´ıas subyacen es, como pueden
T abajo Fin de G ado
10 CAP´
ITULO 2. PRELIMINARES
se : la eo ´ıa de los n´ume os en e os, la eo ´ıa de los eales, la eo ´ıa de los a ays
o la de los bi - ec o s. De es e modo, dada una cie a ´o mula F, y bajo alguna de
las eo ´ıas p e ias, que nos es ingen la in e p e aci´on de los dis in os s´ımbolos que
apa ecen en nues a ´o mula, el p oblema consis e en de e mina si Fes sa is ac ible.
En es e con ex o apa ecen lo que se denominan esolu o es SMT. Se a a
de he amien as enca gadas de decidi la sa is ac ibilidad de una ´o mula conc e a
en su co espondien e eo ´ıa. De en e los muchos que pueden encon a se, uno de
los m´as comple os, y el que m´as se ajus a a nues as necesidades, es Z3. Se a a de
un esolu o SMT c eado po Mic oso Resea ch pa a la p ueba de eo emas y la
comp obaci´on de la sa is ac ibilidad de ´o mulas l´ogicas sob e una se ie de eo ´ıas.
Modos de uso
Un esolu o SMT, como es Z3, p esen a dos modos de uso: de e mina la
sa is ac ibilidad de una se ie de es icciones y ob ene un modelo que las e i ique,
o es ablece la alidez de una ´o mula l´ogica.
En el p ime caso, Z3 abaja con una se ie de decla aciones de a iables y
unciones sob e las cuales se es ablecen una se ie de es icciones pa a que cumplan
cie os equisi os. Una ez de inidas odas es as es icciones median e ase os, se
pide a Z3 que comp uebe si se pueden sa is ace , es deci , que busque si exis e alguna
combinaci´on de alo es pa a las a iables de modo que los ase os sean cie os. En
caso de que s´ı que lo sea, se le puede pedi adem´as que nos de uel a un modelo, es
deci , una asignaci´on de alo es a cada a iable que hace que odas las es icciones
se e i iquen. A la ho a de pedi el modelo nos encon amos una limi aci´on, y es
que ´unicamen e nos de uel e una posible combinaci´on, cuando uno pod ´ıa es a
in e esado en ob ene m´as de una.
En el segundo modo de uso, lo que se busca es de e mina si una cie a
´o mula l´ogica es ´alida, es deci , si es siemp e cie a pa a cualquie combinaci´on de
alo es. Si pidi´e amos a Z3 que comp oba a la sa is ac ibilidad de al ´o mula como
hac´ıamos en el p ime modo de uso, en caso de ob ene que es sa is ac ible quie e
deci que hay al menos una combinaci´on que hace cie a la ´o mula. Pe o es o no nos
es su icien e pues o que noso os necesi amos que sea cie o pa a cualquie asignaci´on
de alo es y no pa a una pa icula . De es e modo, el p ocedimien o consis e en nega
nues a ´o mula y pedi , aho a s´ı, que comp uebe si se puede sa is ace . As´ı, si Z3
nos de uel e que es a ´o mula negada es insa is ac ible, en onces pod emos asegu a
que la o iginal e a ´alida pues o que se hac´ıa cie a pa a alo es cualesquie a.
En e los dos modos de uso explicados, noso os u iliza emos el p ime o de
ellos. Como ya hemos comen ado p e iamen e, buscamos gene a una se ie de casos
de p ueba pa a dis in as unciones y que pueden ene que cumpli una se ie de
condiciones que cons i uyen la p econdici´on. Es as condiciones gene a ´an en onces
una se ie de es icciones que noso os necesi amos que se e i iquen. Adem´as, una
ez sepamos que pueden sa is ace se, nos in e esa ´a ob ene un modelo pa a ales
es icciones, que con o ma ´a nues o caso de p ueba. Sin emba go, nos encon amos
Miguel Ga ido Canalejas
2.3. LA HERRAMIENTA Z3 11
(decla e-cons a In )
(decla e- un (In ) Bool)
(asse (< a 5))
(asse (= ( a) ue))
(check-sa )
(ge -model)
Figu a 2.4: C´odigo de un p og ama b´asico en Z3
con el p oblema de que noso os deseamos ob ene a ios casos de p ueba y, como
hemos comen ado an e io men e, Z3 solo nos de uel e un modelo. Pa a soluciona
es e p oblema la ´ecnica que p oponemos consis e en i a˜nadiendo sucesi amen e
nue as es icciones que nieguen los modelos ob enidos an e io men e. De es e modo,
los nue os modelos end ´an que e i ica se dis in os a los an e io es, ob eniendo
as´ı di e sos casos de p ueba.
Lenguaje
El o ma o de la en ada en Z3 es una ex ensi´on del que se de ine en el
SMT-LIB 2.0 s anda d. Un sc ip de Z3 cons a de una secuencia de comandos que
se almacenan en una pila que el esolu o ges iona in e namen e. En e los comandos
podemos encon a decla aciones de cons an es y unciones (decla e-cons ydecla e-
un espec i amen e); es icciones (asse ), que a˜naden una ´o mula en la pila, y
que se ´an las que el e i icado a e de hace cie as, encon ando una in e p e aci´on
adecuada pa a las unciones y cons an es decla adas; check-sa , que nos se i ´a pa a
de e mina si las ´o mulas almacenadas en la pila son sa is ac ibles o no, de ol iendo
sa ounsa seg´un co esponda; y ge -model que nos de uel e una in e p e aci´on pa a
las cons an es y unciones en caso de que haya sido esuel o como sa is ac ible.
En la Figu a 2.4 puede e se la sin axis conc e a que end ´ıa un peque˜no
p og ama Z3, en el que quedan ecogidos odos los comandos mencionados an e io -
men e. El e i icado a a ´a de da alo es an o a la cons an e ay la unci´on de
o ma que ambos ase os se hagan cie os. En caso de encon a ales alo es, nos
de ol e ´a que es sa is ac ible jun o a un modelo conc e o, y en caso con a io que es
insa is ac ible. Queda e lejado en la Figu a 2.5 lo ob enido pa a es e sencillo caso
de p ueba. Se obse a que ha encon ado una posible asignaci´on de alo es, de modo
que el esul ado es sa , y que dicha asignaci´on nos con o ma un modelo en el que se
iene a=0 y (x)= ue si x=0, o (x)= ue en caso con a io.
T abajo Fin de G ado
12 CAP´
ITULO 2. PRELIMINARES
sa
(model
(de ine- un a () In
0)
(de ine- un ((x!0 In )) Bool
(i e (= x!0 0) ue
ue))
)
Figu a 2.5: Resul ado y modelo de la ejecuci´on del p og ama de la Figu a 2.4
(decla e-cons a In )
(decla e-cons b In )
(decla e-cons c Real)
(decla e-cons d Real)
(asse (< (- a 1) (+ b 2)))
(asse (>= c d))
(check-sa )
(ge -model)
Figu a 2.6: Ejemplo de uso de en e os y eales
Teo ´ıas
Z3 cuen a con esolu o es pa a di e sas eo ´ıas. Con amos a con inuaci´on
aquellas que usa emos du an e el desa ollo de es e abajo.
•A i m´e ica lineal de en e os y eales: decla ados median e el comando
decla e-cons , Z3 nos pe mi e ep esen a y u iliza los n´ume os en e os y eales
ma em´a icos. Pod emos usa los en nues as ´o mulas jun o a di e en es ope a-
do es como +,−, <, e c. (Figu a 2.6). Adem´as, Z3 nos da sopo e pa a ealiza
la di isi´on.
•L´ogica p oposicional: median e el ipo p ede inido Bool podemos abaja
con exp esiones booleanas en Z3. Sopo a los ope ado es usuales and, o , xo ,
no , =>(pa a la implicaci´on), i e (que ep esen a la es uc u a i - hen-else)
y = (pa a la doble implicaci´on). En la Figu a 2.7 podemos e un sencillo
ejemplo de uso de booleanos con di e en es ope ado es. Al pedi que la unci´on
aplicada al alo ue no sea cie a, es deci , que la ama i de dicha unci´on
sea alsa, ob enemos los alo es de ue y alse pa a pyq espec i amen e.
•A ays: Z3 cuen a con una eo ´ıa b´asica de a ays, ep esen ados in e namen e
en o ma de unci´on no in e p e ada de ´ındices en alo es, en p incipio de
dominio in ini o. Quedan ca ac e izados median e dos ope aciones, selec y
Miguel Ga ido Canalejas
2.3. LA HERRAMIENTA Z3 13
(decla e-cons p Bool)
(decla e-cons q Bool)
(decla e-cons Bool)
(de ine- un (( Bool)) Bool
(
i e(= ue)
(=> p q)
(=> q p)
)
)
(asse (no ( ue)))
(check-sa )
(ge -model)
Figu a 2.7: Ejemplo de uso de booleanos
s o e. De es e modo, la ope aci´on (selec a i) nos de uel e el elemen o de
la posici´on idel a ay a; y la ope aci´on (s o e a i ) nos de uel e un a ay
id´en ico a asal o en la posici´on ien la que se encuen a el alo . Cuando
que amos un modelo de un a ay, ob end emos una in e p e aci´on del mismo
en o ma de unci´on, median e el cons uc o (- as-a ay ). Si pa a un
cie o a ay aob enemos al in e p e aci´on, en onces pa a odo ´ındice ise
iene que (selec a i) es igual a ( i). Obse amos en la Figu a 2.8 que
Z3 c ea la unci´on auxilia k!0 pa a da una in e p e aci´on al a ay a . Es a
unci´on nos de uel e: 5 si ecibe un 2; 2 si ecibe un 1; y 5 en cualquie o o
caso. Es o se ajus a a lo eque ido en las dos ´o mulas selec .
•Tipos algeb aicos: encon amos aqu´ı una de las p incipales en ajas de Z3,
que es que nos pe mi i ´a especi ica algunas de las es uc u as de da os m´as
comunes como uplas, ´a boles o lis as. Adem´as, p esen a la opci´on de decla a
ipos ecu si os y mu uamen e ecu si os. Pa a decla a un ipo algeb aico
usa emos el comando decla e-da a ypes, indicando despu´es las cons uc o-
as del ipo.
•Cuan i icado es: Z3 puede abaja con ´o mulas que u ilicen cuan i icado-
es. Pa a maneja ales ´o mulas, u iliza di e sos en oques. Al abaja con
cuan i icado es, el comando check-sa puede de ol e nos un nue o alo , unk-
nown, en caso de no habe podido ins ancia las a iables cuan i icadas, dado
que el p oblema es en gene al indecidible.
T abajo Fin de G ado

14 CAP´
ITULO 2. PRELIMINARES
(decla e-cons a (A ay In In ))
(asse (= (selec a 2) 5))
(asse (= (selec a 1) 2))
(check-sa )
(ge -model)
sa
(model
(de ine- un a () (A ay In In )
(_ as-a ay k!0))
(de ine- un k!0 ((x!0 In )) In
(i e (= x!0 2) 5
(i e (= x!0 1) 2
5))
)
Figu a 2.8: Decla aci´on de a ay e in e p e aci´on en o ma de unci´on
Miguel Ga ido Canalejas
Cap´ı ulo 3
El lenguaje de ase os
En un ase o de la IR pueden apa ece nos exp esiones b´asicas sob e boo-
leanos y en e os, los p ime os elacionados en e s´ı median e los ope ado es l´ogicos
and,o yno , y los segundos elacionados con ope ado es como <, =, ≤, e c. Den-
o de es as exp esiones b´asicas podemos encon a nos ambi´en cuan i icado es (∃y
∀). Pe o adem´as, den o de un ase o podemos encon a nos p edicados y unciones
espec´ı icos de cie os ipos de da os, como pod ´ıan se la longi ud de una lis a, la
o denaci´on de un a ay o la al u a de un ´a bol. Todos es os ase os quedan e lejados
en la Figu a 3.1.
Du an e es a secci´on e emos c´omo ans o ma p edicados a es icciones
Z3, y sob e odo, analiza emos c´omo queda de inido cada ipo algeb aico en Z3 y
odas las ope aciones que pod emos ealiza sob e ellos.
Pe o an es de desa olla odo ello, es con enien e de ene nos en comen-
a dos aspec os de Z3 que esul an de suma impo ancia pa a pode implemen a
an o los ipos algeb aicos como sus di e en es ope aciones. Lo p ime o, como ya
comen amos en la Secci´on 2.3, es la posibilidad de c ea ipos ecu si os, lo que nos
pe mi i ´a c ea elemen os como los ´a boles o las lis as que de o o modo no se ´ıa
posible. El segundo aspec o impo an e es que pod emos abaja con unciones e-
cu si as usando el comando de - un- ec. G acias a es a opci´on de Z3, pod emos
eco e odas las es uc u as ecu si as de mane a c´omoda haciendo los c´alculos
que sean opo unos, que de o o modo, no hab ´ıa sido posible. Y es que, po ejem-
plo, algo an b´asico como calcula la longi ud de una lis a equie e el eco e la
ecu si amen e analizando la cons uc o a y acumulando la longi ud.
3.1. Sin axis b´asica
Las exp esiones m´as b´asicas que podemos encon a nos en un ase o, se ´an
aquellas que ealicen sencillas ope aciones sob e en e os o booleanos. Pa a aba-
ja con ellas en Z3, bas a ´a con c ea ase os independien es en los que se ayan
plasmando ales ope aciones.
15
16 CAP´
ITULO 3. EL LENGUAJE DE ASERTOS
φ::= ue | alse |id {cons an e booleana o a iable }
|id 1· · · n{aplicaci´on de p edicado }
|φ1∧φ2|φ1∨φ2|φ1→φ2|φ1≡φ2| ¬φ{conec i as p oposicionales }
| ∀ idi: ypei. φ | ∃ idi: ypei. φ {ase o cuan i icado }
Figu a 3.1: Sin axis abs ac a de los ase os
(asse (and p q))
(asse (no (and p (o q )))
(asse (=> p (and q ))
Figu a 3.2: Ejemplos sob e exp esiones booleanas
Al abaja con exp esiones booleanas, pod emos encon a nos dis in as
a iables de ipo Bool elacionadas en e s´ı median e ope ado es l´ogicos ales como
and,o ,no , implicaciones, e c. Todas es os ope ado es es ´an a nues a disposici´on
en la pla a o ma Z3, po lo que podemos u iliza los con o al no malidad como
ha ´ıamos en cualquie o o lenguaje. Se mues an en la Figu a 3.2 algunos ejemplos
sencillos sob e ase os con booleanos, donde las a iables p,qy son de ipo Bool.
Po su pa e, con los ase os que impliquen en e os pod emos encon a nos
ope aciones como sumas, es as, mul iplicaciones o di isiones, as´ı como elaciones
de o den ales como ≤, =, e c. De nue o, odos es os ope ado es es ´an a nues a
disposici´on en Z3 po lo que nues os ase os pod ´an inclui los sin p oblema alguno.
Algunos ejemplos sencillos pueden e se en la Figu a 3.3, donde aybson a iables
en e as.
Adem´as de es as ope aciones b´asicas sob e en e os, pod emos encon a nos,
an o en los ase os como en unciones que i emos exponiendo a lo la go de la secci´on,
o as unciones pa a las que Z3 no nos da sopo e y enemos que de ini las noso os.
Se a a de ope aciones pa a encon a el m´aximo o m´ınimo de dos n´ume os (Figu as
3.4 y 3.5 espec i amen e) y pa a ob ene el alo absolu o de un cie o n´ume o
(Figu a 3.6).
3.2. Tipo Lis a
Pa a de ini una lis a lo ha emos de o ma ecu si a siguiendo la idea de
que una lis a es un elemen o seguido de o a lis a. As´ı, las lis as quedan de inidas
en Z3 como puede e se en la Figu a 3.7. Se obse a que las cons uc o as son bien
nil, pa a la lis a ac´ıa, bien cons pa a una lis a no ac´ıa. En es e segundo caso,
siguiendo la idea comen ada p e iamen e, enemos un elemen o de ipo In que se ´a
la cabeza de la lis a y una cola que se ´a o a lis a. Pa a accede a es os dos campos
con amos con los des uc o es hd y l.
De inido ya el ipo, queda e cada una de las ope aciones que pod emos
ealiza sob e ´el. En los ase os, en e los p edicados que e ie en a lis as nos en-
Miguel Ga ido Canalejas
3.2. TIPO LISTA 17
(asse (= a 5))
(asse (> (+ a b) 7)
Figu a 3.3: Ejemplos sob e exp esiones con en e os
(de ine- un
max ((a In ) (b In )) In
(i e(> a b) a b)
)
Figu a 3.4: C´alculo del m´aximo de dos n´ume os
con amos: leng h, pa a calcula la longi ud de una lis a; membe , que nos pe mi e
sabe si un elemen o pe enece a una lis a; so edLis , pa a sabe si una lis a es ´a
o denada; y mul ise , que nos p opo ciona el mul ise de la lis a. Veamos en onces
como queda implemen ada cada una de ellas en Z3.
Longi ud
La ope aci´on leng h, nos de ol e ´a la longi ud de una lis a dada. El c´alculo
de dicha longi ud se ha ´a de o ma ecu si a como puede e se en la Figu a 3.8. Se
obse a que la longi ud se ´a ce o si la lis a es ac´ıa o bien uno m´as la longi ud de
la lis a que con o ma la cola.
Lis a o denada
Con es a ope aci´on comp oba emos si una cie a lis a es ´a o denada o no,
de ol iendo ue o alse espec i amen e. De nue o, es a unci´on se de ine ecu si-
amen e, de mane a que una lis a es ´a o denada si se cumple que el elemen o de la
cabeza de la lis a es meno que el elemen o de la cabeza de la cola y, ambi´en, que
la cola es ´e o denada. Adem´as, an o una lis a ac´ıa como una lis a con un ´unico
elemen o es ´an o denadas. Es a idea queda e lejada en el c´odigo de la Figu a 3.9,
en la que el p ime i e conside a el caso de la lis a ac´ıa, el segundo conside a la
lis a de un solo elemen o, y la pa e del else se ocupa del c´alculo ecu si o.
Pe enencia
Nos encon amos de nue o con una unci´on ecu si a, que nos de ol e ´a
ue en caso de que un elemen o dado pe enezca a una lis a ambi´en dada o alse
en caso con a io. Un elemen o pe enece ´a a una lis a, bien si es la cabeza de la
misma o bien si pe enece a la cola. Ob iamen e, un elemen o no puede pe enece
a una lis a ac´ıa, po lo que el caso b´asico de nues a unci´on en el que la lis a sea
T abajo Fin de G ado
24 CAP´
ITULO 3. EL LENGUAJE DE ASERTOS
(de ine- un
leng hA ((a (A In ))) In
(second a)
)
Figu a 3.17: Longi ud de un a ay
(de ine- un
so edA ((a (A In )) (b1 In ) (b2 In )) Bool
(
o all ((i In ) (j In )) (=> (and (<= b1 i) (<= i j) (< j b2))
(<= (selec ( i s a) i) (selec ( i s a) j)))
)
)
Figu a 3.18: A ay o denado
Al u a
Pa a calcula la al u a de un ´a bol lo ha emos de o ma ecu si a, seg´un
queda de inido en la Figu a 3.23. Dado un cie o ´a bol, la unci´on nos de ol e ´a la
al u a del mismo. Calcula emos la al u a como uno m´as el m´aximo de las al u as de
los hijos izquie do y de echo. En caso de ene un ´a bol ac´ıo, la al u a es ce o. As´ı,
si po ejemplo enemos un ´a bol con un solo nodo, emos que ob end ´ıamos al u a
uno (1 + max(0,0)), como cab ´ıa espe a .
Pa a la llamada ecu si a, emos que llamamos a la unci´on heigh pas´ando-
le como pa ´ame o el esul ado de aplica la cons uc o a izq ode , que es de ipo
T ee, al y como espe a la unci´on.
Al u a m´ınima
La al u a m´ınima de un ´a bol bina io es la al u a o p o undidad desde
la a´ız has a el nodo ac´ıo m´as ce cano. Es deci , es igual que la al u a excep o
que debemos busca el m´ınimo de las al u as de los hijos en ez del m´aximo. La
de inici´on en Z3 (Figu a 3.24) es, po an o, an´aloga a la unci´on heigh , sal o que
en el caso ecu si o, en ez de coge el m´aximo en e las al u as de los hijos, como
hac´ıamos en esa unci´on, aqu´ı end emos que coge el m´ınimo.
Ca dinal
Cuando hablamos del ca dinal de un ´a bol bina io nos e e imos al n´ume o
de elemen os que iene. Es deci , cuan os nodos no ac´ıos, o lo que es lo mismo, que
la cons uc o a no sea lea , nos encon amos. As´ı, el ca dinal de un nodo ac´ıo se ´a
Miguel Ga ido Canalejas

3.4. TIPO ´
ARBOL BINARIO 25
(de ine- un- ec
so edA ((a (A In )) (b1 In ) (b2 In )) Bool
(
i e(>= b1 b2)
ue
(and (<= (selec ( i s a) b1) (selec ( i s a) (+ b1 1)))
(so edA a (+ b1 1) b2))
)
)
Figu a 3.19: Funci´on ecu si a pa a a ays o denados
(de ine- un
mul ise A ((a (A In ))) (Mul ise In )
(mul ise A Aux 0 a)
)
(de ine- un- ec
mul ise A Aux ((i In ) (a (A In ))) (Mul ise In )
(
i e(= i (second a))
emp yMs
(Mse -union (mul ise A (+ i 1) a) (uni Ms (selec ( i s a) i)))
)
)
Figu a 3.20: Funciones pa a calcula el mul ise de un a ay
ce o y el de uno no ac´ıo se ´a uno. Es o queda e lejado con la unci´on ecu si a
ca d de la Figu a 3.25, en la que en el caso base en el que el ´a bol es ac´ıo de uel e
ce o, y en el caso ecu si o hace la suma de los ca dinales de cada uno de los hijos
pa a calcula el es o de nodos y le suma uno po el nodo ac ual.
Se
Dado un ´a bol, podemos es a in e esados en ob ene una ep esen aci´on
del mismo en o ma de Se . El p ime incon enien e que nos encon amos es la
ep esen aci´on de se s en Z3, pues no cuen a con un ipo p opio. La o ma elegida
pa a a a los es como un a ay de alo es de ipo T en booleanos, donde T es el
mismo ipo que el de los alo es del ´a bol (Figu a 3.26), de modo que si un cie o
alo es ´a en el conjun o, a [ ]= ue.
Solucionada la ep esen aci´on del ipo, queda esol e como pasa los alo-
es que nos encon emos en el ´a bol al a ay. Lo hacemos ecu si amen e de modo que
el se de un ´a bol es la uni´on de los se s ob enidos pa a sus dos hijos, unido a su ez
al conjun o uni a io o mado po el elemen o del nodo en el que es emos. Como caso
T abajo Fin de G ado
26 CAP´
ITULO 3. EL LENGUAJE DE ASERTOS
(de ine- un
pe mu ((a1 (A In )) (a2 (A In ))) Bool
(= (mul ise A ( i s a1))
(mul ise A ( i s a2)))
)
Figu a 3.21: Comp obaci´on de si dos a ays son pe mu aci´on el uno del o o
(decla e-da a ypes (T)
((T ee lea (node ( al T) (izq T ee) (de T ee)))))
Figu a 3.22: De inici´on del ipo ´a bol bina io
base end emos el ´a bol ac´ıo pa a el cual debe emos de ol e un conjun o ambi´en
ac´ıo. Po an o, an es de de ini la unci´on Se nos hace al a de ini las unciones
auxilia es emp y, que nos de uel e un se ac´ıo (Figu a 3.27); union, que hace la
uni´on de dos se s (Figu a 3.28); y uni , que se enca ga de c ea un conjun o con un
´unico elemen o (Figu a 3.29). La p ime a de ellas simplemen e inicializa un a ay
con odas sus posiciones a alse. La segunda, g acias al map aplica la ope aci´on o a
cada pa de elemen os de dos a ays dados, es deci , ∀i∈T:se [i] = se 1[i]∨se 2[i].
La e ce a pone a ue la posici´on dada de un a ay ac´ıo.
Vis as ya en onces odas las unciones auxilia es, solo queda e c´omo queda
la unci´on que ob iene el se de un ´a bol. Si el ´a bol es ac´ıo, de ol e ´a un a ay
ac´ıo usando la unci´on emp y. Si, po el con a io, el ´a bol no es ac´ıo, y es amos en
un nodo con alo e hijos izquie do y de echo ly , espec i amen e, de ol e emos:
se (l)∪uni ( )∪se ( ). Todo es o queda e lejado en la Figu a 3.30.
BST
Un ´a bol bina io es de b´usqueda si odos los nodos del hijo izquie do son
meno es que la a´ız, y ´es a a su ez es meno que los nodos del hijo de echo. Adem´as,
ambos hijos izquie do y de echo deben p ese a ambi´en es a p opiedad. As´ı, pa a
comp oba si un ´a bol es un BST end emos que hace lo de o ma ecu si a. Com-
p oba que el o den de los elemen os es el adecuado no puede limi a se a compa a
la a´ız de un ´a bol con los alo es almacenados en los hijos izquie do y de echo, pues
lo que necesi amos es que odos los nodos e i iquen la p opiedad. Usamos en onces,
pa a hace las comp obaciones, el se de los hijos, de modo que odo elemen o del
se del hijo izquie do debe ´a se meno que la a´ız, y odo elemen o del se del hijo
de echo debe ´a se mayo . De es e modo, la unci´on ha ´ıa uso del o all de Z3, a in
de comp oba la p opiedad mencionada pa a odos los elemen os de cada uno de los
se s.
No obs an e, con es a unci´on espe amos ob ene dos uncionalidades. La
p ime a de ellas, comp oba si un ´a bol dado es BST. Pa a es e caso, la de inici´on
apo ada pa a nues a unci´on es pe ec amen e ´alida. La segunda de las uncio-
Miguel Ga ido Canalejas
3.4. TIPO ´
ARBOL BINARIO 27
(de ine- un- ec
heigh (( (T ee In ))) In
(
i e(= lea )
0
(+ 1 (max (heigh (izq )) (heigh (de ))))
)
)
Figu a 3.23: Ope aci´on heigh sob e un ´a bol bina io
(de ine- un- ec
minHeigh (( (T ee In ))) In
(
i e(= lea )
0
(+ 1 (min (minHeigh (izq )) (minHeigh (de ))))
)
)
Figu a 3.24: Al u a m´ınima de un ´a bol
nalidades que espe amos consegui , a pa i de es a unci´on, es la de ellena una
cie a es uc u a de ´a bol con alo es cumpliendo que el ´a bol esul an e sea BST.
Aqu´ı sin emba go encon amos m´as p oblemas con nues a de inici´on, pues o que
al abaja con cuan i icado es Z3 no es capaz de ins ancia co ec amen e las a-
iables de la es uc u a de mane a que espe en las condiciones impues as. Po ello,
debemos ede ini la unci´on sin usa el cuan i icado ni se s.
Conside emos la es uc u a gene al de un ´a bol bina io como en la Figu a
3.31. Tal ´a bol se ´a BST si se e i ica que es mayo que el alo m´ınimo de 1y
meno que el m´aximo de 2. Po an o, lo p ime o que necesi amos es de ini nos en
Z3 dos unciones que se enca guen de calcula los alo es m´ınimo y m´aximo de un
cie o ´a bol. Explicamos la unci´on que calcula el m´ınimo y la enca gada de calcula
el m´aximo es o almen e an´aloga. Dado un ´a bol, pa a encon a el m´ınimo que emos
i eco iendo ecu si amen e los hijos izquie do y de echo y compa ando los alo es
almacenados en los nodos de es os con el alo almacenado en la a´ız. De es e
modo, cuando lleguemos a un nodo ac´ıo le asigna emos un alo su icien emen e
g ande, y en caso de es a en un nodo no ac´ıo de ol e emos el m´ınimo en e el
alo almacenado en dicho nodo y el alo m´ınimo de los ´a boles que con o man
sus dos hijos. Es a idea queda plasmada en la unci´on de la Figu a 3.32 y en la
unci´on equi alen e pa a calcula el m´aximo (Figu a 3.33). Conocidos ya el m´ınimo
y el m´aximo de los dos hijos de un nodo, podemos aplica la idea comen ada pa a
a e igua si es BST y descende ecu si amen e po los hijos comp obando si ´es os
lo son ambi´en. As´ı, la Figu a 3.34 ecoge la unci´on enca gada de comp oba si un
´a bol pasado como pa ´ame o es o no de b´usqueda.
T abajo Fin de G ado
28 CAP´
ITULO 3. EL LENGUAJE DE ASERTOS
(de ine- un- ec
ca d (( (T ee In ))) In
(
i e(= lea )
0
(+ 1 (+ (ca d (izq )) (ca d (de ))))
)
)
Figu a 3.25: Ca dinal de un ´a bol
(de ine-so Se (T) (A ay T Bool))
Figu a 3.26: De inici´on del ipo Se
Mon ´ıculo
Un mon ´ıculo es una pa icula izaci´on de los ´a boles bina ios, donde el
p oblema que p e ende esol e se es el de encon a el elemen o m´ınimo o m´aximo,
seg´un co esponda, y no un elemen o cualquie a. Seg´un el elemen o que desee encon-
a se enemos los minHeaps, en los que hay acceso di ec o al elemen o m´ınimo, y
los maxHeaps, en los que lo hay al m´aximo. Noso os abaja emos con los p ime os.
En un minHeap, la ca ac e ´ıs ica undamen al es que odos los hijos de
un nodo son mayo es o iguales que ´es e, pe o luego en e ellos no hay ninguna
es icci´on adicional. Es o queda e lejado en la unci´on de la Figu a 3.35, en la
que se comp ueba ecu si amen e que se e i ique es a p opiedad. En el p ime i
conside amos el caso en el que el ´a bol sea ac´ıo y en el segundo enemos que el
´a bol es ´a o mado po un ´unico nodo, cumpli´endose en ambos casos que el ´a bol
es un mon ´ıculo y de ol iendo po an o ue. En el e ce i conside amos que solo
uno de los hijos sea ac´ıo, conc e amen e el izquie do, de modo que en esa ama solo
enemos que comp oba los alo es de la a´ız y del hijo de echo, mien as que en el
cua o hacemos lo mismo pe o conside ando es a ez que el hijo ac´ıo es el de echo.
Po ´ul imo, en la ama del else inal encon amos el caso en que ambos hijos sean
no ac´ıos, pa a el cual debemos hace odas las comp obaciones en e el alo de la
a´ız y los de los hijos.
Po o o lado, un mon ´ıculo sesgado equie e habe sido o mado median-
e dos mon ´ıculos sesgados p e ios usando mezcla sesgada. Es a p opiedad esul a
imposible de especi ica en Z3, y ampoco nos esul a de g an in e ´es, po ello,
conside a emos, como ´unica es icci´on de es e ipo de mon ´ıculos, la que e ie e al
o den de sus elemen os como en el es o de mon ´ıculos. Po an o, nos bas a ´a con
comp oba la unci´on de la Figu a 3.35 pa a a i ma si un mon ´ıculo es sesgado.
Miguel Ga ido Canalejas
3.5. TIPO ´
ARBOL AVL 29
(de ine- un emp y () (Se In )
((as cons (A ay In Bool)) alse))
Figu a 3.27: Funci´on emp y
(de ine- un se -union ((s1 (Se In )) (s2 (Se In ))) (Se In )
((_ map o ) s1 s2 ) )
Figu a 3.28: Funci´on union
Zu do
Uno de los ipos de mon ´ıculos m´as in e esan es que nos encon amos son
los mon ´ıculos zu dos. Pa a la de inici´on de un mon ´ıculo zu do es necesa io usa la
al u a m´ınima de inida p e iamen e en es a secci´on. Un mon ´ıculo es zu do en onces
si es ac´ıo, o si ambos hijos son zu dos y adem´as la al u a m´ınima del hijo izquie do
es mayo o igual que la del hijo de echo. Es a idea queda e lejada en Z3 en la unci´on
ecu si a de la Figu a 3.36. Po an o, un mon ´ıculo debe cumpli , pa a se zu do,
an o la unci´on an e io isHeap, como es a, zu do.
3.5. Tipo ´
A bol AVL
Un ´a bol AVL es un ipo especial de ´a bol bina io en el que en cada nodo,
adem´as de almacena un cie o alo , gua damos ambi´en la al u a a la que se
encuen a dicho nodo en el ´a bol. Po ello, la ep esen aci´on en Z3 es o almen e
id´en ica a la de los ´a boles bina ios, pe o a˜nadiendo simplemen e un campo m´as
a la cons uc o a node que e ie a a la al u a del nodo (Figu a 3.37). Adem´as, los
´a boles AVL son ´a boles de b´usqueda, po lo que los elemen os debe ´an man ene
un cie o o den, pe o cuen an con una ca ac e ´ıs ica adicional, que es que la al u a
debe man ene el ´a bol equilib ado, es o es, la di e encia en e las al u as de los dos
hijos de un nodo cualquie a no puede se mayo que uno.
La mayo ´ıa de los c´ompu os que necesi emos ealiza sob e un AVL se ´an
los mismos que hac´ıamos con los ´a boles bina ios: calcula la al u a median e una
unci´on heigh ; calcula el n´ume o de elemen os o ca dinal; y a e igua su se .
Adem´as de es as unciones ya conocidas, que debe ´an se ede inidas pa a el ipo
AVL, apa ece una nue a unci´on, isAVL, enca gada de comp oba que se e i iquen
odas las condiciones necesa ias pa a que un ´a bol bina io sea un AVL.
T abajo Fin de G ado

30 CAP´
ITULO 3. EL LENGUAJE DE ASERTOS
(de ine- un uni ((i In )) (Se In )
(s o e emp y i ue))
Figu a 3.29: Funci´on uni
(de ine- un- ec
se (( (T ee In ))) (Se In )
(
i e(= lea )
emp y
(se -union (se -union (se (izq )) (se (de ))) (uni ( al )))
)
)
Figu a 3.30: Funci´on que calcula el se de un ´a bol bina io
Al u a
Calcula la al u a de un ´a bol AVL espe a la idea seguida con los ´a boles
bina ios. A sabe , la al u a de un nodo se ´a uno m´as el m´aximo de las al u as de sus
dos hijos. Po ello, la de inici´on de la unci´on queda exac amen e igual que es aba
pa a ales ´a boles, con la ´unica sal edad de que hay que enomb a las cons uc o as.
En la Figu a 3.38 queda e lejada es a unci´on.
Ca dinal
Del mismo modo que con la al u a, calcula el ca dinal es igual pa a los
´a boles AVL que pa a los bina ios. Po ello, la unci´on de la Figu a 3.39, enca ga-
da de hace al c´alculo, queda de inida del mismo modo que la de la Figu a 3.25
enomb ando las cons uc o as que apa ezcan.
Se
Una ez m´as, nos encon amos con una unci´on que no p esen a di e encias
con la u ilizada pa a ´a boles bina ios, m´as all´a de los enomb amie os opo unos.
Calcula el se de un ´a bol AVL se hace del mismo modo que con ´a boles bina ios,
es deci , si enemos un ´a bol ac´ıo el conjun o de uel o es ambi´en ac´ıo, y pa a un
nodo no ac´ıo el conjun o se ob iene de ealiza la uni´on en e los se s de los dos
hijos y el conjun o uni a io o mado po el alo almacenado en dicho nodo. Po
ello, se ha ´a uso aqu´ı ambi´en de las unciones auxilia es de inidas pa a los ´a boles
bina ios, a sabe , emp y (Figu a 3.27), uni (Figu a 3.29), y se -union (Figu a 3.28).
La unci´on gene al que calcula el se del ´a bol queda de inida en la Figu a 3.40.
Miguel Ga ido Canalejas
3.5. TIPO ´
ARBOL AVL 31
Figu a 3.31: Es uc u a gene al de un ´a bol bina io
(de ine- un- ec
minT (( (T ee In ))) In
(
i e(= lea )
2000
(min ( al ) (min (minT (izq )) (minT (de ))))
)
)
Figu a 3.32: C´alculo del alo m´ınimo de un ´a bol
BST
Pa a que un ´a bol sea AVL end ´a que cumpli que sea de b´usqueda. Po
ello, necesi amos ede ini el p edicado isBST de la Figu a 3.34. La idea seguida es
la misma, pues los elemen os deben man ene el mismo o den que impon´ıamos en al
unci´on. Po an o, ´unicamen e debemos p eocupa nos de enomb a las unciones
auxilia es (Figu a 3.41 y Figu a 3.42) y modi ica , an o en ellas como en la p incipal
(Figu a 3.43), las di e en es apa iciones de las cons uc o as de nues o ipo de da os.
AVL
Como comen ´abamos al p incipio de la secci´on, un ´a bol AVL no deja de se
un ´a bol bina io de b´usqueda, con la ´unica pa icula idad de que iene una cie a
imposici´on sob e las al u as. Se ´an en onces es as las es icciones que debamos
comp oba a la ho a de de e mina si un cie o ´a bol es o no un AVL.
En p ime luga , po se un ´a bol de b´usqueda end emos que ecu i
al p edicado isBST que nos de e mina si el o den de los elemen os en los nodos
es el adecuado. En segundo luga , hay que comp oba que la di e encia de al u as
en e ambos hijos no sea mayo que uno. Po ´ul imo, pa a que un cie o ´a bol sea
T abajo Fin de G ado
32 CAP´
ITULO 3. EL LENGUAJE DE ASERTOS
(de ine- un- ec
maxT (( (T ee In ))) In
(
i e(= lea )
-2000
(max ( al ) (max (maxT (izq )) (maxT (de ))))
)
)
Figu a 3.33: M´aximo de un ´a bol
(de ine- un- ec
isBST (( (T ee In ))) Bool
(
i e(= lea )
ue
(i e (and (= (izq ) lea ) (= (de ) lea ))
ue
(i e (= (izq ) lea )
(and (isBST (de )) (< ( al ) (minT (de ))))
(i e (= (de ) lea )
(and (isBST (izq )) (< (maxT (izq )) ( al )))
(and (and (isBST (izq )) (isBST (de )))
(and (< (maxT (izq )) ( al )) (< ( al ) (minT (de )))))
)
)
)
)
)
Figu a 3.34: Funci´on que comp ueba si un ´a bol es BST
AVL, adem´as de cumpli es as dos condiciones an e io es, iene que cumpli ambi´en
que sus dos hijos sean ambi´en AVL. Po ello, la comp obaci´on debe ´a hace se de
mane a ecu si a, conside ando como caso base el ´a bol ac´ıo, el cual s´ı es AVL. La
unci´on de la Figu a 3.44 plasma odas es as ideas. Obse amos que en la ama i
comp obamos si el ´a bol es ac´ıo, de ol iendo ue en al caso, y que en la ama
del else hacemos las llamadas ecu si as con los hijos izquie do y de echo como
pa ´ame os, adem´as de comp oba que sea BST y que se cumpla la di e encia de
al u as eque ida, siendo absol la unci´on alo absolu o de inida como en la Secci´on
3.1 de es e cap´ı ulo. Adem´as de odo es o, enemos que a˜nadi una condici´on especial.
Si eco damos la de inici´on de un ´a bol AVL, en´ıamos un campo ese ado en cada
nodo pa a almacena su al u a. Pues bien, es e alo debe se co ec o, es deci , debe
se e ec i amen e la al u a de dicho nodo. Po ello, al comp oba que un ´a bol sea
AVL ha emos ambi´en al comp obaci´on, lo que se educe a e si el alo gua dado
en el nodo es igual a uno m´as el m´aximo de las al u as de sus hijos.
Miguel Ga ido Canalejas
3.5. TIPO ´
ARBOL AVL 33
(de ine- un- ec
isHeap (( (T ee In ))) Bool
(
i e(= lea )
ue
(i e (and (= (izq ) lea ) (= (de ) lea ))
ue
(i e(= (izq ) lea )
(and (< ( alue ) (minT (de ))) (isHeap (de )))
(i e(= (de ) lea )
(and (< ( alue ) (minT (izq ))) (isHeap (izq )))
(and (and (< ( al ) ( al (izq ))) (< ( al ) ( al (de ))))
(and (isHeap (izq )) (isHeap (de ))))
)
)
)))
Figu a 3.35: Funci´on isHeap
(de ine- un- ec
isLe is (( (T ee In ))) Bool
(
i e (= lea )
ue
(and (and (isLe is (izq )) (isLe is (de )))
(>= (minHeigh (izq )) (minHeigh (de ))))
)
)
Figu a 3.36: Funci´on que comp ueba si un ´a bol bina io es zu do
Es a unci´on es la p incipal de los ´a boles AVL y nos p opo ciona ´a dos usos un-
damen ales. El p ime o y m´as b´asico es comp oba si el ´a bol que ecibe como
pa ´ame o e i ica odas las condiciones que debe cumpli pa a se AVL. No obs-
an e, el uso m´as in e esan e es ellena una cie a es uc u a de o ma que el ´a bol
esul an e sea AVL. De es e modo, un cie o ´a bol con es uc u a de AVL, pe o
con a iables desconocidas como campos de cada uno de los nodos, puede pasa se
a la unci´on como pa ´ame o y que ´es a nos de alo es a cada una de las a iables,
an o las de alo como las de al u a, cumpliendo odas ellas odos los equisi os
necesa ios.
T abajo Fin de G ado
40 CAP´
ITULO 3. EL LENGUAJE DE ASERTOS
(de ine- un- ec
ca dL (( (LLRB In ))) In
(
i e(= lea L)
0
(+ 1 (+ (ca dL (izq )) (ca dL (de ))))
)
)
Figu a 3.49: Ca dinal de un ´a bol ojineg o
(de ine- un- ec
se L (( (LLRB In ))) (Se In )
(
i e(= lea L)
emp y
(se -union (se -union (se L (izq )) (se L (de ))) (uni ( al )))
)
)
Figu a 3.50: Ob enci´on del se de un LLRB
de la unci´on goodColo .
3.7. Doble uso de los p edicados
Du an e la explicaci´on de algunos de los m´e odos ya hemos ido in odu-
ciendo la idea de que p esen aban dos modos de uso. Es e plan eamien o equie e
abo da lo con algo m´as de de enimien o pues es lo m´as inno ado que nos apo -
a es e abajo. Si eco damos, en cap´ı ulos p e ios dec´ıamos que has a aho a la
gene aci´on de casos de p ueba consis ´ıa en gene a di e en es casos y il a los des-
ca ando aquellos que no e an ´alidos, y que noso os a a ´ıamos de gene a los
siendo di ec amen e buenos. Pues bien, es p ecisamen e es e doble uso de los p edi-
cados de inidos el que nos pe mi e hace es o sin pe de la capacidad de il a en
caso de necesi a lo.
En p ime luga , el uso m´as b´asico que podemos hace es el de il a de
mane a cl´asica. Dado un cie o alo pa a una a iable, cualquie a que sea su ipo,
pod emos llama a una cie a unci´on que noso os engamos de inida que ealice
una se ie de comp obaciones sob e ella y nos diga si cumple una se ie de condiciones
o no. Has a aqu´ı, no encon amos nada nue o, pues o que es o puede hace se con
cualquie unci´on que nos de inamos en cualquie lenguaje de p og amaci´on.
En segundo luga , podemos usa los p edicados de Z3 pa a asigna alo es
a a iables cumpliendo una se ie de condiciones. Y es aqu´ı donde se nos p esen an
las opciones m´as no edosas e in e esan es, pues, es amos en onces en condiciones
Miguel Ga ido Canalejas

3.7. DOBLE USO DE LOS PREDICADOS 41
(de ine- un
goodColo (( (LLRB In ))) Bool
(
i e(= lea L)
ue
(i e(= (colo ) Neg o)
(=> (= (ge Colo (de )) Rojo) (= (ge Colo (izq )) Rojo))
(and (= (ge Colo (izq )) Neg o) (= (ge Colo (de )) Neg o))
)
)
)
Figu a 3.51: Funci´on goodColo pa a ´a boles ojineg os
(de ine- un
ge Colo (( (LLRB In ))) Bool
(
i e(= lea L)
Neg o
(colo )
)
)
Figu a 3.52: Funci´on ge Colo pa a ´a boles ojineg os
de da le di ec amen e alo es buenos a una a iable, en luga de pe de ecu sos
en asigna le alo es alea o ios y luego comp oba si nos alen o no. Po ejemplo,
de mane a muy sencilla, si una cie a a iable a necesi amos que sea meno que
es, con el p ime en oque end ´ıamos que da le alo es alea o ios y luego desca -
a mien as que con el segundo podemos consegui que au om´a icamen e ome un
alo que nos in e ese. Es o que pod ´ıa pa ece i ele an e con a iables y es ic-
ciones an sencillas, puede aplica se a cualquie a iable de cualquie ipo, y es ah´ı
donde ob enemos la e dade a po encia de es e m´e odo de u ilizaci´on de nues os
p edicados.
Conside emos po ejemplo una cie a a iable de ipo T ee. Es a a iable
iene cinco nodos pa a los que necesi amos ob ene unos alo es que nos e i iquen
una se ie de es icciones de o den, po ejemplo, que es ´en o denadas de mane a que
el ´a bol sea de b´usqueda. Si solo con ´a amos con el p ime m´e odo de uso comen ado,
end ´ıamos que limi a nos a c ea ´a boles de cinco nodos con alo es alea o ios en
cada uno de ellos, y pasa los po nues o m´e odo co espondien e pa a comp oba si
es ´an o denados como dese´abamos. No obs an e, con la segunda posibilidad podemos
almacena en cada nodo una cie a a iable, de modo que al pedi le a Z3 que e i ique
la unci´on co espondien e, ´el solo sea capaz de da nos alo es buenos pa a cada uno
de es os nodos aho ´andonos an o la gene aci´on au om´a ica como el il ado.
No obs an e, se encuen an algunas limi aciones en es e modo de uso. Y es
T abajo Fin de G ado
42 CAP´
ITULO 3. EL LENGUAJE DE ASERTOS
(de ine- un- ec
isBSTL (( (LLRB In ))) Bool
(
i e(= lea L)
ue
(i e (and (= (izq ) lea L) (= (de ) lea L))
ue
(i e (= (izq ) lea L)
(and (isBSTL (de )) (< ( al ) (minTL (de ))))
(i e (= (de ) lea L)
(and (isBSTL (izq )) (< (maxTL (izq )) ( al )))
(and (and (isBSTL (izq )) (isBSTL (de )))
(and (< (maxTL (izq )) ( al )) (< ( al ) (minTL (de )))))
)
)
)
)
)
Figu a 3.53: Funci´on que comp ueba si un ´a bol ojineg o es de b´usqueda
(de ine- un- ec
isLl bAux (( (LLRB In ))) Bool
(
i e(= lea L)
ue
(and (isBSTL ) (and (and (and (isLl bAux (izq )) (isLl bAux (de )))
(goodColo )) (eq (blackHeigh (izq )) (blackHeigh (de )))))
)
)
Figu a 3.54: Funci´on isLl bAux
que, a la ho a de c ea a iables de un ipo algeb aico pe demos es a po encia. Po
ejemplo, al y como hemos is o, unciones como la enca gada de calcula el ca dinal
de un ´a bol o la al u a del mismo, es ´an de inidas de mane a ecu si a. Po ello, si
noso os pidi´e amos a Z3 que in en a a da le alo a una a iable de ipo T ee,
que es un ipo algeb aico de inido ambi´en ecu si amen e, cumpliendo que u ie a
un cie o ca dinal o una cie a al u a, Z3 es incapaz de encon a una asignaci´on
pa a nues a a iable . Po ello, pa a es os ipos de es icciones no nos queda ´a
m´as emedio que a a las con el p ime o de los en oques comen ados.
Se ´a du an e el cap´ı ulo p ´oximo cuando en emos en de alle a comen a
como hemos decidido esol e es as limi aciones, in en ando exp imi la po encia
de Z3 al m´aximo cuando sea posible, clasi icando las es icciones en di e en es i-
pos. Comen a emos ambi´en a qu´e ipo de es icciones pe enecen cada una de las
unciones is as a lo la go de es e cap´ı ulo y con ello el en oque de uso que les damos.
Miguel Ga ido Canalejas
3.7. DOBLE USO DE LOS PREDICADOS 43
(de ine- un
isLl b (( (LLRB In ))) Bool
(
and (= (ge Colo ) Neg o) (isLl bAux )
)
)
Figu a 3.55: Funci´on isLl b
A modo de conclusi´on, se incluye un peque˜no ejemplo con el que ilus a
es as ideas que acabamos de comen a . Supongamos que enemos una a iable que
es un ´a bol bina io ( ipo T ee). Abo demos p ime o las limi aciones. Si pedimos a
Z3 que a e de e i ica una es icci´on del es ilo (asse (= (ca d ) 4)), en la
que se equie e que el ca dinal de sea cua o, nos encon amos que Z3 se queda blo-
queado, incapaz de esol e es e p oblema. Comen amos aho a los di e en es modos
de uso. Man engamos la misma a iable , pe o es a ez con una es uc u a ya de ini-
da, po ejemplo (node x1 (node x2 lea lea ) (node x3 lea lea )), donde
cada a iable xi e ie e al alo almacenado en cada nodo. Si le pedimos a Z3 que e-
i ique la es icci´on (asse (= (ca d ) 3)), en la que se le pide que el ca dinal
sea es, ac ua ´a en modo de il o calculando el ca dinal de nues o ´a bol y de ol-
i´endonos sa ounsa seg´un cumpla la es icci´on o no. Po o o lado, si u ilizamos
una es icci´on del ipo (asse (isBST )), es amos pidiendo a Z3 que e i ique
que el ´a bol es de b´usqueda. Pues bien, es aqu´ı donde en a en juego el segundo mo-
do de uso, pues Z3 no solo nos de uel e sa en caso de que pueda ellena se, sino que
nos de uel e ambi´en alo es pa a cada a iable xi, a sabe , x1= 1999, x2=−1999
yx3= 2001. Es os alo es son alea o ios pe o cumplen el o den eque ido.
T abajo Fin de G ado
44 CAP´
ITULO 3. EL LENGUAJE DE ASERTOS
Miguel Ga ido Canalejas
Cap´ı ulo 4
Es a egia de gene aci´on de casos
Como ya hemos mencionado, es e abajo iene po obje i o la gene a-
ci´on de casos de p ueba que se ajus en au om´a icamen e a las p econdiciones del
p og ama que deseemos p oba . Pa a ello, esul a con enien e ans o ma ales p e-
condiciones en una secuencia de es icciones. As´ı, con es as es icciones y g acias
a la po encia de Z3, pod emos ob ene un modelo que cumpla odas ellas, es deci ,
un caso de p ueba de nues o p og ama o almen e ´alido.
Pa a pode gene a los casos de p ueba co ec amen e, en p ime luga he-
mos enido que clasi ica las es icciones que puede in e esa nos a a en di e en es
g upos, como e emos en la p ime a secci´on de es e cap´ı ulo. Una ez de e mina-
das las di e en es es icciones y elegido el m´e odo seguido pa a a a cada una
de ellas, solo queda ans o ma la IR a un conjun o de es icciones p ocesables
po Z3, c eando pa a ello un a chi o de o ma o sm . Comen a emos, po an o, en
la segunda secci´on de es e cap´ı ulo la es a egia seguida pa a lle a es e p oceso a
cabo. Habla emos ambi´en de las limi aciones encon adas y como las hemos ido
sol en ando.
4.1. Tipos de es icciones
Como ya se in odujo en la Secci´on 3.7, las di e en es unciones de Z3
pod´ıan se u ilizadas de di e sas mane as, encon ´andonos p oblemas cuando que-
´ıamos cons ui un elemen o de ipo algeb aico a pa i de una al u a o un n´ume o
de elemen os. Es as unciones se u iliza ´an po p econdiciones que puedan eque-
i las. Po an o, es as di e encias en e m´e odos de u ilizaci´on de unas unciones
y o as de i a en que debemos a a de mane a di e en e los ase os que podamos
encon a nos en las p econdiciones. Cada ase o al inal impone un es icci´on sob e
una cie a a iable, po lo que lo que ha emos es clasi ica las es icciones en es
g andes g upos: es icciones de ama˜no, es icciones de es uc u a y es icciones
de con enido.
45

46 CAP´
ITULO 4. ESTRATEGIA DE GENERACI´
ON DE CASOS
4.1.1. Res icciones de ama˜no
Tal y como su nomb e indica, hacen e e encia al ama˜no de las di e en-
es es uc u as que puedan apa ece nos. Se ´an en onces la unci´on leng hA pa a
a ays, leng h pa a lis as y ca d pa a ´a boles. Pa a a ays, si eco damos, la longi ud
no e a m´as que un campo de una upla, po lo que no hab ´ıa m´as que c ea nos una
es icci´on pa a asigna el alo deseado a al campo y end ´ıamos ya la longi ud del
a ay. No obs an e, pa a lis as y ´a boles, que son ipos algeb aicos, nos encon amos
el p oblema mencionado en la Secci´on 3.7, a sabe , Z3 no puede c ea una es uc u a
a pa i de un cie o ama˜no. Po ello, es as unciones se ´an a adas como me os
elemen os de e i icaci´on y no pa a c ea a iables. De es a mane a, pod emos u i-
liza las pa a comp oba si el ama˜no de una es uc u a es el eque ido, en caso de
que la p econdici´on nos lo pida.
4.1.2. Res icciones de es uc u a
Aplicadas exclusi amen e a ´a boles, abaja ´an sob e la es uc u a de los
mismos, es deci , sob e aspec os como la al u a, la al u a m´ınima, los colo es, la
al u a neg a...
Con es as es icciones desea ´ıamos ob ene ´a boles ac´ıos, es deci , que no
engan ning´un da o almacenado, y que se ajus en a la es uc u a pedida. Po ejem-
plo, supongamos una cie a p econdici´on que nos pide que la di e encia de al u as
en e los hijos izquie do y de echo de un ´a bol no sea mayo que uno (condici´on
in e na de se AVL), nos gus a ´ıa que Z3 nos cons uye a un ´a bol adecuado a es o.
Es deci , pedi le a Z3 que nos esuel a una ´o mula del es ilo
(asse (= (di Heigh ) ue)),
siendo di Heigh una supues a unci´on que comp uebe la condici´on sob e las al u as
mencionada an e io men e, y una cons an e del ipo T ee de inido como en la
Secci´on 3.4, y que nos cons uya di ec amen e como noso os que emos. Pues
bien, nos en en amos de nue o a la limi aci´on comen ada de Z3, pues o que no es
capaz de ealiza al a ea.
Vis os en onces los p oblemas encon ados con es e ipo de ase os, eamos
c´omo a a los pa a sal a es as di icul ades. Como ya hac´ıamos con las es icciones
de ama˜no, nos limi a emos a a a es as es icciones como elemen os de e i ica-
ci´on. De es e modo, s´ı pod emos e i ica que un ´a bol e i ique que cumple alguna
cie a p opiedad es uc u al.
Las es icciones es uc u ales acos umb an a eni incluidas den o de p e-
dicados m´as gene ales, po ejemplo, un ´a bol AVL debe cumpli cie as condiciones
sob e las al u as de los hijos o un ´a bol ojineg o debe cumpli que las al u as neg as
de cada hijo sean iguales. Sin emba go, o os p edicados son pu amen e es uc u a-
les, como es el caso de que un mon ´ıculo sea zu do. Pa a los p ime os, las llamadas
Miguel Ga ido Canalejas
4.1. TIPOS DE RESTRICCIONES 47
a es as unciones nos e i ica ´an in e namen e que se cumpla la es icci´on es uc-
u al eque ida, de ol iendo unsa en caso de no hace lo. Si lo e i ica, p osegui ´a
con el es o de comp obaciones aunque pod ´ıa alla po o o lado po alguna o a
es icci´on. Po su pa e, pa a los segundos, la llamada comp oba ´a exclusi amen e
la es icci´on es uc u al de ol i´endonos di ec amen e si se cumple o no. Ilus amos
es as ideas con dos ejemplos. Si yo pido a Z3 que e i ique la siguien e es icci´on
(asse (isAVL )),
con un ´a bol AVL y la unci´on isAVL de inida como en la Figu a 3.44, comp oba ´a
aspec os sob e las al u as de los hijos, en e o as conside aciones. Sin emba go, si
yo pido e i ica una es icci´on como
(asse (isLe is )),
donde es un ´a bol bina io e isLe is co esponde a la unci´on de inida en la Fi-
gu a 3.36, es amos a ando con una unci´on pu amen e es uc u al que solo hace
comp obaciones sob e las al u as m´ınimas.
Concluimos las es icciones de es uc u a con algunos casos pa icula es,
que son la al u a neg a de los ´a boles ojineg os y la al u a de los ´a boles AVL.
Al a a se de al u as, es amos e iden emen e an e es icciones es uc u ales, con
las mismas limi aciones que el es o, es deci , no podemos cons ui un ´a bol desde
ce o a pa i de una se ie de aspec os sob e la al u a neg a. De es e modo, po
ejemplo pa a la p ime a, end emos que u iliza la pa a e i ica si una es uc u a de
´a bol ojineg o iene una al u a neg a u o a y e si se adap a a lo necesi ado. Sin
emba go, la al u a neg a, en e o as cosas analiza los colo es de los nodos. Tales
colo es, si eco damos, e an un campo m´as de un ´a bol ojineg o, al que espe amos
da le un alo . Es deci , los colo es son pa e del con enido del ´a bol. Po ello,es as
es icciones e e idas a la al u a neg a, si bien no pueden cons ui un ´a bol, pod ´an
se i nos como es icciones de con enido, al y como explica emos a con inuaci´on,
pa a da alo es a los colo es. Lo mismo ocu e en onces con el campo de al u a
almacenado en un ´a bol AVL y las es icciones sob e la al u a de es os ´a boles.
4.1.3. Res icciones de con enido
T abaja ´an sob e el con enido de nues a es uc u a, es deci , sob e los
da os que la compongan. Es as es icciones, al con a io que las an e io es, nos
pe mi en los dos m´e odos de usos comen ados en la Secci´on 3.7. Podemos, po un
lado, comp oba si una a iable con cie os alo es gua dados cumple una es ic-
ci´on y, po o o lado, ellena una es uc u a conc e a. El en oque e dade amen e
in e esan e y no edoso es el segundo, y es el que apo a la po encia a es e abajo,
pues nos se i ´a pa a c ea odos los alo es sin necesidad de il a los despu´es. Nos
cen a emos en onces en ´es e, analizando como ellena es uc u as. Comen a emos
p ime o los casos elemen ales de con enido, pa a luego analiza las pa icula idades
in oducidas en las es icciones es uc u ales.
T abajo Fin de G ado
48 CAP´
ITULO 4. ESTRATEGIA DE GENERACI´
ON DE CASOS
(decla e-cons u (A In ))
(decla e-cons (A In ))
(asse (= (second u) 4))
(asse (= (second ) 4))
(asse (pe mu u ))
Figu a 4.1: Comp obaci´on de la pe mu aci´on de dos a ays
(de ine- un k!19 ((x!0 In )) In
(i e (= x!0 2) 11
(i e (= x!0 3) 7
(i e (= x!0 1) 7
(i e (= x!0 0) 7
5)))))
(de ine- un k!20 ((x!0 In )) In
(i e (= x!0 2) 7
(i e (= x!0 3) 7
(i e (= x!0 1) 11
(i e (= x!0 0) 7
6)))))
Figu a 4.2: Modelo ob enido as ejecu a la unci´on pe mu
Cuando hablamos de con enido, hablamos de los alo es almacenados en
a ays, lis as o ´a boles. Dis inguimos la o ma de abaja con a ays espec o a las
o as dos. Y es que, al ene Z3 sopo e pa a a ays, la o ma de c ea con enido puede
hace se de o ma m´as di ec a que en los o os casos. Comen amos cada pe spec i a.
Al abaja con a ays, Z3 nos p opo ciona una ep esen aci´on in e na en
o ma de unci´on. Las unciones so edA ype mu abajan sob e el con enido
de los a ays. Pues bien, simplemen e llamando a la p ime a con un a ay de una
longi ud de e minada, Z3 nos c ea ´a di ec amen e los alo es almacenados en cada
posici´on del a ay e i icando la p opiedad de o den. Po su pa e, pa a la segunda,
si le pasamos dos a ays con una cie a longi ud ijada pa a cada uno de ellos (misma
longi ud pues iene que habe el mismo n´ume o de elemen os), de nue o Z3 c ea los
dos a ays co ec amen e. Pe o adem´as, no solo es capaz de c ea ambos a ays de
ce o, sino que, en caso de que uno de los dos enga ya alo es y el o o no, puede
ellena las dis in as posiciones del segundo con los elemen os que con o man el
p ime o, e i icando que el a ay esul an e sea pe mu aci´on del de pa ida. Vemos
en la Figu a 4.1 qu´e ocu e al llama a la unci´on pe mu aci´on. Los dos a ays se
c ean ac´ıos, y ´unicamen e se les asigna una longi ud a cada uno de ellos. El modelo
ob enido (Figu a 4.2) e i ica que el a ay u, de inido como la unci´on k!19, iene
los mismos elemen os que , que co esponde a la unci´on k!20, aunque en dis in o
o den, es deci , e ec i amen e uno es pe mu aci´on del o o.
Miguel Ga ido Canalejas
4.2. ESTRATEGIA 49
Po su pa e, al abaja con lis as o ´a boles la a ea se uel e algo m´as
compleja. Al con a io que pa a los a ays, la de inici´on de es os ipos no es in e na
de Z3 sino que nos la hemos c eado noso os con nues os ipos algeb aicos co es-
pondien es. Po ello, pa a abaja con cualquie elemen o de uno de es os ipos
necesi amos ene especi icada p e iamen e una es uc u a conc e a. Es a es uc u-
a end ´a ac´ıa, es deci , con los nodos sin ning´un alo almacenado en ellos, sino con
a iables del ipo que co esponda seg´un el campo, que son las que espe amos que
Z3 nos ins ancie con alo es adecuados. Po an o, al con a io que con los a ays,
en los que nos bas aba de ini la a iable y da le una longi ud, aqu´ı end emos que
da le a la a iable conc e a una cie a es uc u a.
Comen amos, po ´ul imo, esa dualidad pa a algunas de las es icciones
de es uc u a. Como hemos mencionado, aspec os como la al u a de un AVL o la
al u a neg a de un ´a bol ojineg o e ie en a campos del p opio ipo de da os. Po
ello, pod emos usa las ambi´en pa a ellena es os pa ´ame os. De es e modo, si
a una cie a es uc u a de ´a bol de ipo LLRB le pedimos que comp uebe que sea
e ec i amen e ojineg o, es deci , llamamos a la unci´on isLl b de la Figu a 3.55, en e
las comp obaciones que ealiza encon amos algunas que se e ie en a los colo es, y
en e ellas la de las al u as neg as de los hijos. As´ı, odas es as es icciones en
conjun o nos de ol e ´ıan alo es pa a cada uno de los colo es de los nodos. En la
Figu a 4.3, emos que apa ece decla ado un ´a bol ojineg o, adem´as de una se ie
de a iables en e as y de colo pa a cons ui la es uc u a del ´a bol. Pues bien,
al pedi que comp uebe la unci´on isLl b, ob enemos el modelo de la Figu a 4.4,
en el que podemos e que el ´a bol ha quedado comple amen e ins anciado, con
odas las a iables de colo omando un alo conc e o. En la Figu a 4.5 podemos
e la ep esen aci´on del modelo en o ma de ´a bol, a in de hace m´as c´omoda la
in e p e aci´on de los alo es ob enidos. El ´a bol ob enido es e ec i amen e un ´a bol
ojineg o co ec o.
4.2. Es a egia
Has a aho a hemos is o c´omo abaja con cada ipo de es icci´on. A
con inuaci´on, e emos c´omo es a dis inci´on nos acili a ´a la gene aci´on de casos g a-
cias a la es a egia seguida. Podemos dis ingui cua o e apas: ija un ama˜no pa a
los casos de p ueba, gene a es uc u as de ese ama˜no, aplica las es icciones de
es uc u a co espondien es a las es uc u as gene adas y po ´ul imo popula ales
es uc u as. Con es as e apas lo que se p e ende es sal a las limi aciones de Z3 a la
ho a de abaja con las es icciones de ama˜no y es uc u a y ap o echa despu´es
su po encia al a a las de con enido. Como Z3 no es capaz de gene a es uc u as
dado un cie o ama˜no, las dos p ime as e apas se ealizan desde Haskell. Despu´es,
las es uc u as c eadas se pasan a Z3, donde se esuel en las siguien es dos e apas,
consiguiendo pobla ales es uc u as y ob eniendo, con ello, nues o caso de p ueba
inal.
T abajo Fin de G ado
56 CAP´
ITULO 5. EXPERIMENTOS
Funci´on En ada P econdici´on Desc ipci´on
Inse Lis x:In , l :Ls {so edLis (l)}Inse a el elemen o xo denada-
men e en l
Dele eLis x:In , l :Ls {membe (x, l)}Elimina el elemen o xde la lis a
l
Tabla 5.1: Funciones pa a lis as
cada caso los esul ados ob enidos pa a di e en es ama˜nos de lis a.
So ed
Nues a in enci´on aqu´ı es pobla di e en es es uc u as de lis as con una
longi ud dada, cumpliendo que la lis a esul an e es ´e o denada. Con el in de apo a
una can idad de ejemplos su icien es, abaja emos lis as de ca dinales desde dos
has a seis. Enume amos a con inuaci´on odos los esul ados ob enidos pa a cada
uno de esos ama˜nos:
•(cons 0 (cons 1 nil))
•(cons (- 1) (cons 0 (cons 1 nil)))
•(cons 0 (cons 1 (cons 2 (cons 3 nil))))
•(cons 0 (cons 1 (cons 2 (cons 3 (cons 4 nil)))))
•(cons (- 1) (cons 0 (cons 1 (cons 2 (cons 3 (cons 4 nil))))))
Puede e se que en odos ellos, la lis a gene ada es ´a o denada, de modo
que Z3 es ´a poblando co ec amen e nues as es uc u as de lis a.
Membe
Si en el caso an e io busc´abamos lis as o denadas, aqu´ı el o den de los
elemen os no nos in e esa, lo ´unico impo an e es que el elemen o xpe enezca a
la lis a. Po an o, Z3 no solo iene la a ea de gene a la lis a, sino que adem´as
debe ´a ins ancia esa a iable xcon un cie o alo y asegu a que ´es e sea uno de
los elemen os que la con o man. De nue o, es udia emos las lis as gene adas seg´un
los ama˜nos elegidos. Quedan enume adas a con inuaci´on odas es as lis as jun o al
alo asignado a la a iable x:
Miguel Ga ido Canalejas

5.2. ARRAYS 57
Funci´on En ada P econdici´on Desc ipci´on
Inse A x:In , m :
In , a :A ay
{0≤m < leng h(a)∧
so edA (a, 0, m)}
Inse a el elemen o xen el
a ay a
Tabla 5.2: Funciones pa a a ays
•x=0: (cons 0 (cons (- 2) nil))
•x=0: (cons 0 (cons (- 2) (cons 2 nil)))
•x=0: (cons 0 (cons (- 2) (cons 2 (cons 3 nil))))
•x=0: (cons 0 (cons (- 2) (cons 2 (cons 3 (cons 3 nil)))))
•x=0: (cons 0 (cons (- 2) (cons 2 (cons 3 (cons 3 (cons 4 nil))))))
En odos los casos encon amos que el alo asignado a xes ce o, y que
es e alo se encuen a en odas las lis as. Po ello, el modelo p opo cionado po Z3
pa a cada ama˜no es ambi´en co ec o en es e caso.
A in de p oba alg´un esul ado di e en e, a˜nadimos manualmen e una es-
icci´on en la que o cemos a la xa oma un alo di e en e de ce o o uno. El modelo
que p opo ciona en onces Z3, pa a una lis a de cinco elemen os, es:
•x=2: (cons 2 (cons 0 (cons (-2) (cons 2 (cons 3 nil)))))
5.2. A ays
El p edicado m´as impo an e que nos encon amos pa a a ays es so edA ,
que comp ueba si un cie o a ay es ´a o denado en e dos posiciones dadas. Pa a
p oba al p edicado, hemos usado la unci´on de inse ci´on que apa ece en la Tabla
5.2. Vemos que la unci´on ecibe como pa ´ame o un a ay, el elemen o a inse a en
´el y la posici´on en la que hace lo (m). La p econdici´on equie e que la posici´on en
la que inse a es ´e den o de los l´ımi es del a ay, y que ´es e es ´e o denado en e el
p incipio y dicha posici´on. De es e modo, dado que la p econdici´on a ec a an o al
a ay como al pa ´ame o de en ada m, Z3 debe ´a encon a alo es adecuados pa a
ambos. Comen a emos algunos esul ados ob enidos pa a di e en es longi udes del
a ay de en ada.
En p ime luga conside amos como longi ud del a ay cua o. El modelo
de uel o po Z3 puede e se en la Figu a 5.1. Vemos que el a ay iene de inido a
pa i de la unci´on k!0. Es a unci´on de uel e: -2 si ecibe un 0; 2 si ecibe un 1;
y 3 en cualquie o o caso. Adem´as, la a iable mha omado el alo ce o. Es o
quie e deci que el a ay debe es a o denado en e las posiciones ce o y ce o, lo que
es i ial y se cumple sea cual sea el alo que le haya dado al a ay, as´ı que, en
pa icula , nues os alo es lo cumplen.
T abajo Fin de G ado
58 CAP´
ITULO 5. EXPERIMENTOS
(de ine- un a () (Pai (A ay In In ) In )
(mk-pai (_ as-a ay k!0) 4))
(de ine- un m () In
0)
(de ine- un k!0 ((x!0 In )) In
(i e (= x!0 1) 2
(i e (= x!0 0) (- 2)
3)))
Figu a 5.1: Modelo pa a a ay de longi ud cua o
(de ine- un a () (Pai (A ay In In ) In )
(mk-pai (_ as-a ay k!0) 5))
(de ine- un m () In
0)
(de ine- un k!0 ((x!0 In )) In
(i e (= x!0 1) 2
(i e (= x!0 0) (- 2)
(i e (= x!0 4) 4
3)))
Figu a 5.2: Modelo pa a a ay de longi ud cinco
Vamos a conside a aho a que la longi ud del a ay es cinco. En es e caso,
el modelo que nos p opo ciona Z3 es el de la Figu a 5.2. De nue o, la m oma el
alo ce o, as´ı que azonando del mismo modo que hemos hecho an es, podemos
a i ma que el a ay p opo cionado po Z3 es co ec o.
Que Z3 ins ancie la msiemp e a ce o es un caso que epi e cualquie a que
sea la longi ud que le pongamos al a ay. Es os casos, como ya hemos is o son
i iales as´ı que amos a o za a busca alg´un caso algo m´as complicado. Pa a ello,
omamos a ays de longi ud seis y, a˜nadi emos manualmen e dos es icciones con
las que p ohibi a Z3 que le de a la a iable mlos alo es ce o o uno. Con odo
es o, el modelo que nos p opo ciona el esolu o es el que apa ece en la Figu a 5.3.
En es e caso, Z3 ha elegido cinco como alo pa a la m. Po an o, la p econdici´on
pide en es e caso que el a ay comple o es ´e o denado. Si nos ijamos en la unci´on
k!0 que es la que de ine a nues o a ay, emos que de uel e -1 en caso de ecibi
como en ada un ce o, un 3 en caso de ecibi un 5, y un 0 en cualquie o o caso. Si
ep esen amos es a unci´on en o ma de a ay como en la Figu a 5.4, se e ´acilmen e
que el a ay cumple que es ´a o denado.
Miguel Ga ido Canalejas
5.3. ´
ARBOLES BINARIOS 59
(de ine- un a () (Pai (A ay In In ) In )
(mk-pai (_ as-a ay k!0) 6))
(de ine- un m () In
5)
(de ine- un k!0 ((x!0 In )) In
(i e (= x!0 5) 3
(i e (= x!0 0) (- 1)
0)))
Figu a 5.3: Modelo pa a a ay de longi ud seis con mdis in o de ce o o uno
Figu a 5.4: Modelo de a ay de ca dinal seis
5.3. ´
A boles Bina ios
Los ´a boles bina ios si en pa a ep esen a di e en es es uc u as. De en e
las m´as in e esan es, las que decidimos a a en el Cap´ı ulo 3 ue on los mon ´ıculos,
conc e amen e los zu dos, y los ´a boles de b´usqueda (BST). Po ello, las unciones
es udiadas a lo la go de es a secci´on e e i ´an a ambos ipos.
5.3.1. Mon ´ıculos Zu dos
Den o de los dis in os ipos de mon ´ıculos, uno de los m´as in e esan es a
p oba son los zu dos, pues o que nos apo an una cla a sepa aci´on en e p opiedades
es uc u ales, e e idas a las al u as m´ınimas, y de con enido, sob e el o den de los
elemen os den o del ´a bol. De es e modo, los p edicados m´as impo an es a la
ho a de abaja con es os mon ´ıculos son isLe is , enca gado de comp oba si la
es uc u a es adecuada, e isHeap, que ha ´a lo p opio con el con enido. Po an o,
las unciones que amos a analiza incluyen en sus p econdiciones ales p edicados,
como puede e se en la Tabla 5.3.
Dado que los p edicados de ambas p econdiciones son los mismos, u iliza-
emos la p ime a pa a analiza los esul ados ob enidos pa a di e en es ca dinales, y
despu´es mos a emos algunos de los modelos p opo cionados pa a la segunda, a in
de e el compo amien o de Z3 al abaja con dos es uc u as a la ez. As´ı, pa a
la p ime a unci´on comen a emos p ime o los modelos pa a ca dinales dos y es,
analiza emos algunos de ca dinales supe io es y e emos al inal una es ad´ıs ica de
casos acep ados y echazados. Po su pa e, pa a la segunda, aplica emos a las dos
es uc u as que pa icipan los dis in os azonamien os expues os pa a la an e io
unci´on, iendo algunos esul ados pa a ca dinales di e en es.
T abajo Fin de G ado
60 CAP´
ITULO 5. EXPERIMENTOS
Funci´on En ada P econdici´on Desc ipci´on
Inse Le x:In , :T ee {isLe is ( )∧
isHeap( )}
Inse a xen el
mon ´ıculo
UnionLe 1 : T ee, 2 : T ee {(isLe is ( 1)∧
isHeap( 1)) ∧
(isLe is ( 2) ∧
isHeap( 2))}
Une dos mon ´ıculos
zu dos
Tabla 5.3: Funciones pa a mon ´ıculos zu dos
(a) (b)
Figu a 5.5: Es uc u as de un ´a bol bina io de dos nodos
An es de en a a comen a los esul ados, con iene eco da las dos es-
icciones que deben cumpli se. En p ime luga , debe ocu i que la al u a m´ınima
del hijo izquie do debe se mayo o igual que la del hijo de echo y, en segundo luga ,
el alo almacenado en la a´ız debe se meno o igual que el de sus hijos.
Cuando abajamos con ´a boles de ca dinal dos, ´unicamen e podemos en-
con a nos dos es uc u as di e en es, que apa ecen en la Figu a 5.5. Resul a sencillo
e que la p ime a de las es uc u as s´ı que cumple la es icci´on es uc u al eque i-
da, pues o que la al u a m´ınima del hijo izquie do es uno mien as que la del de echo
es ce o, pe o que, po el con a io, la segunda la incumple ya que la al u a m´ınima
del hijo de echo es uno, que es mayo que la del hijo izquie do que es ce o. Como
e a de espe a , al ejecu a nues as es icciones en Z3 ob enemos que e ec i amen e
el caso co espondien e a la segunda es uc u a es insa is ac ible. Po su pa e, pa a
el p ime o ob enemos el modelo (node 0 (node 3 lea lea ) lea ), que cum-
ple que la a´ız es meno que el hijo izquie do, como dese´abamos. Puede e se la
ep esen aci´on del modelo ob enido en o ma de ´a bol en la Figu a 5.6.
Al abaja con ca dinal es, el n´ume o de es uc u as posibles c ece a
cinco, ep esen adas odas ellas en la Figu a 5.7. Dado que la condici´on es uc u al
que iene que cumpli se equie e que la al u a m´ınima del hijo izquie do sea mayo o
igual que la del de echo, emos ´apidamen e que las es uc u as de las Figu as 5.7d
y 5.7e no pod ´an sa is ace nues a p econdici´on. Pe o adem´as, la p opiedad pa a se
zu do e a ecu si a, de modo que los hijos ambi´en deben cumpli la. Si nos ijamos
en la es uc u a de la Figu a 5.7b, emos que pa a el hijo izquie do, sus espec i os
hijos incumplen la p opiedad sob e las al u as m´ınimas. Pues bien, al pasa nues o
iche o de es icciones po Z3, ob enemos unsa como esul ado pa a es as es
es uc u as y sa pa a el es o. As´ı, pa a es as es uc u as sa is ac ibles ob enemos
Miguel Ga ido Canalejas
5.3. ´
ARBOLES BINARIOS 61
Figu a 5.6: Modelo pa a mon ´ıculo zu do de ca dinal dos
adem´as los modelos (node (-3) (node (-3) (node 0 lea lea ) lea ) lea )
pa a la Figu a 5.7a y (node 0 (node 2 lea lea ) (node 4 lea lea )) pa a
la Figu a 5.7c. Ambos modelos ob enidos apa ecen e lejados en la Figu a 5.8
A pa i de aqu´ı e emos solo algunos ejemplos in e esan es de modelos
ob enidos pa a ca dinales supe io es. En la Figu a 5.9a se mues a un modelo de-
uel o po Z3 pa a una es uc u a de ca dinal cua o. En p ime luga , e i ica
e iden emen e la p opiedad es uc u al, pues o que si no ue a as´ı no hab ´ıa podido
esol e la. Es una es uc u a in e esan e pues o que, al ene dos nodos en el hijo
de echo y solo uno en el izquie do pod ´ıa lle a nos a enga˜no. Sin emba go, la al u a
m´ınima del hijo de echo es uno, igual que la del izquie do. En segundo luga , emos
que los alo es asignados a cada nodo cumplen se meno es o iguales que los de sus
espec i os hijos. Con odo ello, el modelo ob enido es co ec o. Po su pa e, en
las Figu as 5.9b y 5.9c apa ecen dos nue os modelos, uno de ca dinal cinco y o o
de ca dinal seis. De nue o, si nos ijamos en los alo es p opo cionados po Z3 pa a
ellena cada uno de los nodos, emos que ambos modelos uel en a se co ec os
pues o que espe an el o den eque ido, al cumpli se siemp e que la a´ız es meno o
igual que sus hijos.
Pa a la segunda unci´on, la ´unica di e encia es que en ez de abaja sob e
una ´unica es uc u a lo ha emos sob e dos, y en consecuencia, la p econdici´on a ec a
a ambas, comp obando que sean mon ´ıculos zu dos. As´ı, las condiciones a cumpli
son exac amen e las mismas, po lo que los azonamien os a la ho a de iden i ica
es uc u as ´alidas son o almen e an´alogos a los ealizados has a aho a con la p i-
me a unci´on. De es e modo, si po ejemplo, enemos un caso en el que se combinan
las es uc u as de las Figu as 5.7c y 5.5b, la p ime a cumpli ´ıa las es icciones pe o
la segunda no, de mane a que la es icci´on de i ada de la p econdici´on se ´ıa insa-
is ac ible. Po el con a io, si po ejemplo se han combinado las es uc u as de las
Figu as 5.7a y 5.7c, al se ambas ´alidas, como ya imos p e iamen e, la es icci´on
en es e caso s´ı se ´ıa sa is ac ible, y Z3 de ol e ´ıa los modelos ap opiados. A in de
mos a un ejemplo con el que ilus a que e ec i amen e ellena co ec amen e dos
es uc u as, en la Figu a 5.10 puede e se el modelo ob enido pa a dos ´a boles, el
p ime o de ca dinal es y el segundo de ca dinal cua o, ambos co ec os an o
es uc u almen e como en lo que e ie e al o den de sus elemen os.
Po ´ul imo, en la Tabla 5.4 se mues an el n´ume o de casos sa is ac ibles e
insa is ac ibles ob enidos pa a ca dinales cua o, cinco y seis.
T abajo Fin de G ado

62 CAP´
ITULO 5. EXPERIMENTOS
(a) (b) (c)
(d) (e)
Figu a 5.7: Es uc u as de un ´a bol bina io de es nodos
5.3.2. ´
A boles de B´usqueda
Las unciones u ilizadas pa a p oba los ´a boles de b´usqueda apa ecen des-
c i as en la Tabla 5.5. Todas ellas eciben como pa ´ame o de en ada una a iable
de ipo T ee, y compa en como p econdici´on la llamada al p edicado isBST, enca -
gado de comp oba si un cie o ´a bol es o no de b´usqueda. Pa a analiza los esul a-
dos ob enidos, mos a emos los modelos ob enidos pa a es uc u as de ca dinal dos
y es, luego comen a emos algunos modelos in e esan es de ama˜no cua o o cinco.
Si eco damos la unci´on isBST de Z3, expues a en el Cap´ı ulo 3, no p esen aba
ninguna es icci´on de ca ´ac e es uc u al, y ´unicamen e se limi aba a comp oba
que los elemen os es u ie an o denados de mane a adecuada. Po ello, pa a odas
las es uc u as ob end emos que la es icci´on isBST es sa is ac ible, jun o a un
modelo adecuado pa a cada una de ellas. Po an o, no en a emos a analiza la
posible sa is ac ibilidad de las di e en es es uc u as, pues o que odas an a se lo,
sino que ´unicamen e es udia emos los esul ados ob enidos a in de e si cumplen
lo espe ado.
Pa a ´a boles bina ios de ca dinal dos, encon amos ´unicamen e dos posi-
bles es uc u as. Al ejecu a Z3, los modelos ob enidos son (node 1 (node 0 lea
lea ) lea ) pa a la es uc u a de la Figu a 5.5a y (node (- 1) lea (node 0
lea lea )) pa a la es uc u a de la Figu a 5.5b. En ambos casos, los alo es asig-
Miguel Ga ido Canalejas
5.3. ´
ARBOLES BINARIOS 63
(a) (b)
Figu a 5.8: Mon ´ıculos zu dos de es nodos
Ca dinal Casos Sa is ac ibles Casos Insa is ac ibles
Cua o 4 10
Cinco 8 34
Seis 17 115
Tabla 5.4: Resul ados ob enidos pa a mon ´ıculos zu dos
nados a los nodos son co ec os pues o que, en el p ime o, la a´ız es mayo que el
hijo izquie do, y en el segundo, la a´ız es meno que el hijo de echo. Tales modelos
pueden e se ep esen ados en o ma de ´a bol en la Figu a 5.11.
Cuando el ca dinal es es, pasamos de ene dos posibles es uc u as a
cinco (Figu a 5.7), odas ellas sa is ac ibles como comen ´abamos p e iamen e. As´ı,
el esul ado de ejecu a Z3 sob e nues as es icciones, son cinco modelos di e en es
pa a las cinco es uc u as. Es os modelos quedan e lejados en la Figu a 5.12, en
la que podemos e odas las es uc u as de ca dinal es pobladas con di e en es
alo es. Vemos que en cada una de ellas, si descendemos po los di e en es sub´a boles,
siemp e se cumple que el hijo izquie do sea meno que la a´ız, y ´es a a su ez sea
meno que el hijo de echo. Po an o, odos los modelos p opo cionados po Z3 son
co ec os.
A pa i de aqu´ı, el n´ume o de es uc u as gene adas c ece no ablemen e,
po lo que solo mos a emos algunos ejemplos de ca dinales cua o y cinco con los
que e mina de con i ma que Z3 es ´a poblando co ec amen e nues os ´a boles. En
la Figu a 5.13 encon amos es posibles modelos pa a ca dinal cua o, mien as que
en la Figu a 5.14 apa ecen dos al e na i as pa a ca dinal cinco. En odas ellas, de
nue o, se e i ica que el o den de los elemen os es co ec o.
T abajo Fin de G ado
64 CAP´
ITULO 5. EXPERIMENTOS
(a) Ca dinal cua o (b) Ca dinal cinco
(c) Ca dinal seis
Figu a 5.9: Mon ´ıculos zu dos de ca dinales cua o, cinco y seis
5.4. ´
A boles AVL
Pa a p oba los ´a boles AVL hemos u ilizado las unciones de inse ci´on de
un elemen o, b´usqueda de un elemen o, y bo ado de un elemen o. En la Tabla 5.6
quedan ecogidas odas es as unciones con sus espec i as p econdiciones, jun o a
algunos da os adicionales. Puede e se que en odas ellas se ecibe como en ada
de la unci´on un ´a bol de ipo AVL, sob e el que ac ´uan odas las p econdiciones
equi iendo que sea, e ec i amen e, un AVL. Dado que odas las p econdiciones son
en onces iguales, no sepa a emos po casos sino que analiza emos odas po igual,
comen ando los esul ados ob enidos pa a di e en es ama˜nos de en ada. Comen-
za emos analizando los esul ados pa a ama˜nos dos y es, comen a emos algunos
casos ep esen a i os pa a ama˜nos mayo es y, po ´ul imo, pa a ama˜nos mayo es
analiza emos el n´ume o de es uc u as echazadas y acep adas, a in de sabe cuan as
se pueden pobla de odas las que se gene an.
Los ´a boles AVL con aban con un campo adicional pa a almacena la al u a
de cada nodo, po lo que, pa a e que el ´a bol c eado po Z3 es co ec o, end emos
que ija nos an o en el o den de los elemen os como en es e da o. Adem´as, con iene
eco da que la p opiedad es uc u al que debe cumpli un ´a bol pa a se AVL es
Miguel Ga ido Canalejas
5.4. ´
ARBOLES AVL 65
(a) (b)
Figu a 5.10: Mon ´ıculos zu dos de ca dinales es y cua o pa a la unci´on de uni´on
Funci´on En ada P econdici´on Desc ipci´on
Inse BST x:In , :T ee {isBST ( )}Inse a el elemen o xen el
´a bol
Sea chBST x:In , :T ee {isBST ( )}Busca el elemen o xen el
´a bol
Dele eBST x:In , :T ee {isBST ( )}Elimina el elemen o xdel
´a bol
Tabla 5.5: Funciones pa a ´a boles bina ios de b´usqueda
que la di e encia en e las al u as de los hijos no sea mayo que uno. A lo la go de la
secci´on, cuando comen emos los casos desca ados nos e e i emos a es a p opiedad.
Si enemos ´a boles bina ios de ca dinal dos, ´unicamen e podemos encon-
a nos dos es uc u as, una con la a´ız y un nodo en el hijo izquie do, y la o a con
la a´ız y un nodo en el de echo. Ambas es uc u as e i ican se AVL, pues o que
en los dos casos la di e encia de al u as de los hijos no es mayo que uno. Po ello,
cab ´ıa espe a que, al pedi a Z3 que esuel a nues as es icciones, ob u i´e amos
que odos los casos son sa is ac ibles, y nos p opo ciona a, po an o, un modelo
pa a nues as es uc u as e i icando ales es icciones. En e ec o, Z3 esuel e los
dos casos como sa y de uel e el modelo (nodeA 3 2 (nodeA 0 1 lea A lea A)
lea A) pa a el ´a bol con hijo de echo ac´ıo (Figu a 5.5a), y (nodeA (- 1) 2 lea A
(nodeA 0 1 lea A lea A)) pa a el de hijo izquie do ac´ıo (Figu a 5.5b). En ambos
casos, en cada nodo, el campo ese ado pa a la al u a oma los alo es espe ados
(dos pa a la a´ız y uno pa a el hijo), mien as que los alo es almacenados espe an
el o den eque ido pa a se ´a bol de b´usqueda, pues o que, en el p ime caso, la a´ız
es mayo que el hijo izquie do, y en el segundo, la a´ız es meno que el hijo de echo.
En la Figu a 5.15 se mues an ambos modelos en o ma de ´a bol.
Con los ´a boles de ca dinal es empiezan a c ece el n´ume o de es uc-
u as gene adas, ecogidas odas ellas en la Figu a 5.7. De en e las cinco posibles
es uc u as, ´unicamen e aquella con un nodo como hijo izquie do y o o como hijo
T abajo Fin de G ado
72 CAP´
ITULO 5. EXPERIMENTOS
Funci´on En ada P econdici´on Desc ipci´on
Inse LLRB x:In , :LLRB {isLLRB( )}Inse a el elemen o xen el
´a bol
Sea chLLRB x:In , :LLRB {isLLRB( )}Busca el elemen o xen el
´a bol
Dele eLLRB¨
Ix:In , :LLRB {isLLRB( )}Elimina el elemen o xdel
´a bol
Tabla 5.8: Funciones pa a ´a boles ojineg os
Figu a 5.19: Modelo pa a un ´a bol de dos nodos
cenados en el sub´a bol izquie do, y meno que aquellos almacenados en el de echo,
cumpliendo as´ı que sea BST. Po o o lado, espec o a los colo es, espe an que las
al u as neg as son iguales pa a cualquie camino desde la a´ız a un nodo ac´ıo y,
adem´as, el ´unico nodo ojo que nos apa ece es ´a a la izquie da. Po odo ello, el
modelo p opo cionado es o almen e co ec o.
Po o o lado, un posible modelo pa a ´a boles de ca dinal cinco es el e le-
jado en la Figu a 5.21b. En ´el emos que po cualquie camino que elijamos la al u a
neg a es siemp e dos, po lo que se espe a la p ime a de las condiciones pa a que
es ´e co ec amen e colo eado. Adem´as, los dos nodos ojos que nos encon amos no
es ´an consecu i os y, aunque hay uno ojo como hijo de echo de un nodo, el co es-
pondien e hijo izquie do es ambi´en ojo. Po odo ello, los colo es p opo cionados
po Z3 son co ec os. Respec o a los alo es que encon amos, ambi´en espe an el
o den eque ido, po lo que, en conjun o, odo el modelo uel e a se co ec o.
Po ´ul imo, pa a ca dinal seis comenzamos a ob ene modelos m´as in e e-
san es con los que mos a la po encia de Z3, pues empieza a ene que al e na
colo es en los di e en es caminos. Uno de los modelos ob enidos es el de la Figu a
5.21c. En ´el podemos e como, a lo la go del hijo izquie do, a al e nando nodos
de colo neg o y ojo, a in de consegui espe a odas las condiciones eque idas.
Vemos que la p ime a de ellas, e e ida a las al u as neg as de los hijos, se cumple,
pues o que po odos los posibles caminos desde la a´ız a un nodo ac´ıo encon a-
mos la misma al u a neg a. Po su pa e, las e e idas a los nodos ojos ambi´en se
cumplen, pues o que no encon amos ni dos nodos ojos seguidos ni un nodo ojo
como hijo de echo siendo el hijo izquie do neg o. Po an o, odos los equisi os sob e
el colo eado del ´a bol se sa is acen. Po su pa e, en lo que e ie e al o den de los
Miguel Ga ido Canalejas

5.5. ´
ARBOLES ROJINEGROS 73
Figu a 5.20: Modelo pa a un ´a bol de ca dinal 3
Ca dinal Casos Sa is ac ibles Casos Insa is ac ibles
Cua o 2 12
Cinco 3 39
Seis 4 128
Tabla 5.9: Resul ados ob enidos pa a ´a boles LLRB
alo es almacenados, ambi´en se cumple la condici´on impues a pa a se BST. Con
odo ello, el modelo analizado es co ec o.
Pa a conclui , en la Tabla 5.9 quedan ecogidos los da os sob e el n´ume o
de casos sa is ac ibles e insa is ac ibles seg´un el ca dinal del ´a bol. Podemos e
que son muy pocas las es uc u as que Z3 puede ellena , pues o que la mayo ´ıa de
los casos son insa is ac ibles. Si bien de p ime as puede esul a chocan e que sean
an as las es uc u as desca adas, odas las es icciones de colo son, en conjun o,
an es ic i as, que es o puede ocu i . Y es que, en p ime luga , en odas aquellas
es uc u as en las que no haya un cie o equilib io en e los nodos que encon amos
a la izquie da y la de echa de la a´ız, esul a ´a imposible consegui que las al u as
neg as sean iguales. Desca adas odas es as, a´un eniendo ese cie o equilib io, hay
muchas en las que el hijo izquie do de un nodo es ac´ıo mien as que el de echo
no lo es, y a ´es e le co esponde ´ıa el colo ojo, si uaci´on p ohibida ambi´en. En
conclusi´on, esul a muy complicado e i ica odas las es icciones in oluc adas en
el p edicado isLLRB, haciendo as´ı que muchas de las es uc u as gene adas sean
desca adas.
Viendo que son an as las es uc u as echazadas, pod ´ıa pensa se que
nues o sis ema no es ´a apo ando ninguna mejo ´ıa. Si conside amos la gene aci´on
de casos de p ueba an e io , en la que se gene aba alea o iamen e la es uc u a, la
p obabilidad de que ue a mala, y po an o desca ada, e a igual que en nues o
caso, pues o que las comp obaciones a ealiza son exac amen e las mismas. Sin
emba go, adem´as de gene a se alea o iamen e la es uc u a, se gene aban ambi´en
los alo es almacenados en ella y los colo es de cada nodo. Es os alo es deb´ıan pasa
el co espondien e il o, haciendo que, aunque la es uc u a ue a co ec a, hubie a
que desca a la po incumpli ales alo es alguna p opiedad. Es o en cambio no
ocu e en nues o sis ema, pues o que una ez enemos las es uc u as buenas, es
imposible que los alo es que las ellenen sean inco ec os.
T abajo Fin de G ado
74 CAP´
ITULO 5. EXPERIMENTOS
(a) Ca dinal 4 (b) Ca dinal 5
(c) Ca dinal 6
Figu a 5.21: Modelos pa a ca dinales cua o, cinco y seis
Pa a conclui la secci´on, amos a analiza , en ´e minos de e iciencia, el
compo amien o de nues o sis ema. Lo hacemos pa a ´a boles ojineg os ya que son
los que ienen que hace mayo n´ume o de comp obaciones y gene a los modelos
m´as complejos, siendo po an o en los que peo es esul ados pueden ob ene se. En
p ime luga , menciona que al p opo ciona nos Z3 un modelo, ´es o no solo consis e
en da alo a las a iables sino que odas las unciones decla adas o man pa e del
modelo. Po an o, pa e del iempo lo ocupa en esc ibi odas es as unciones pa a
cada modelo y, del mismo modo, la mayo pa e de las l´ıneas del iche o de salida
se co esponden con odas ellas. Po ello, los esul ados mos ados a con inuaci´on
son, p ime o con ando con la esc i u a de odas es as unciones pa a cada modelo, y
despu´es eniendo solo en cuen a la esoluci´on de la sa is ac ibilidad de cada posible
es uc u a. En la Tabla 5.10 se mues an los iempos de ejecuci´on pa a gene a odos
los modelos de di e en es ca dinales, p ime o eniendo que esc ibi odo el modelo
y despu´es eniendo en cuen a solo la esoluci´on de la sa is ac ibilidad de cada caso.
Vemos que has a ca dinal seis los iempos son bas an e bajos, pe o a pa i de
ca dinal ocho se dispa an. Es o pa ece l´ogico pues enemos has a 1430 es uc u as
Miguel Ga ido Canalejas
5.5. ´
ARBOLES ROJINEGROS 75
Ca dinal Tiempo modelo comple o Tiempo sa is ac ibilidad
T es 0.134s0.128s
Cua o 0.222s0.163s
Cinco 0.481s0.369s
Seis 1.149s1.018s
Ocho 12.075s11.645s
Tabla 5.10: Tiempos de ejecuci´on
di e en es. O o aspec o que se obse a es que di ie en poco los iempos con modelo
de los de sin modelo. El n´ume o de es uc u as echazadas pa a es os ´a boles e a
muy ele ado, po lo que son pocos los modelos que iene que esc ibi en el p ime o
de los casos. Po ´ul imo, espec o al n´ume o de l´ıneas del iche o inal de salida,
mos amos solo alg´un da o con el que hace nos a la idea de lo que ocupa cada cosa.
Si omamos po ejemplo es uc u as de ca dinal cinco, el iche o ob enido cons a de
871 l´ıneas. Sin emba go, si cogemos uno de los modelos p opo cionados, esul a que
solo 25 son de las a iables que nos in e esan, mien as que 240 son del es o de
unciones. Po an o, se ´a p incipalmen e es o ´ul imo lo que haga que el n´ume o de
l´ıneas se ele e cuando engamos m´as casos sa is ac ibles y, po an o, m´as modelos.
T abajo Fin de G ado
76 CAP´
ITULO 5. EXPERIMENTOS
Miguel Ga ido Canalejas
Cap´ı ulo 6
Conclusiones
Cas ellano
Llegados has a es e pun o, podemos a i ma que los obje i os que se ma -
ca on al comienzo del abajo han sido cumplidos.
Como p ime g an obje i o, nos plan eamos se capaces de ans o ma un
ase o-p econdici´on en un conjun o de es icciones. G acias al p og ama Haskell
c eado, expues o en el Ap´endice A, podemos ans o ma la p econdici´on de una
unci´on, dada en su ep esen aci´on in e media, en una se ie de es icciones p oce-
sables po Z3 con las que gene a au om´a icamen e casos de p ueba a pa i de su
sa is ac ibilidad
Po o o lado, se plan e´o como segundo e o la in es igaci´on de los esolu-
o es SMT, conc e amen e de Z3, con la in enci´on de codi ica en es a pla a o ma
odos los posibles p edicados in oluc ados en las dis in as p econdiciones de algunas
de las unciones m´as in e esan es sob e las es uc u as de da os a adas. Du an-
e el Cap´ı ulo 3, abo damos la explicaci´on de la ans o maci´on de los di e en es
ase os en unciones de Z3, mos ando adem´as la po encia de es a he amien a pa-
a da alo a las di e en es a iables in oluc adas en las es icciones plan eadas.
Los esul ados desp endidos de es a in es igaci´on ue on dispa es. Y es que, si bien
se ha descubie o que es muy po en e a la ho a de da alo a a iables de ipos
sencillos como en e os o a ays, cuando iene que sin e iza es uc u as algeb aicas
como ´a boles o lis as, es incapaz de hace lo. Sin emba go, g acias a la es a egia
plan eada sob e sepa a las es icciones en di e en es ipos, hemos log ado sal a
es a di icul ad de Z3, consiguiendo que nues o sis ema sea bas an e e icaz.
Con odo es o, hemos log ado cumpli la a ea de gene a casos de p ueba
que sa is agan una cie a p econdici´on, pa iendo ´unicamen e de la especi icaci´on de
la misma.
Respec o a las l´ıneas de abajo a segui en un u u o, la p incipal am-
pliaci´on del p oyec o eside en hace uso de la API de Z3 pa a Haskell. Median e
su u ilizaci´on, se ´an dos las p incipales en ajas que se puedan ob ene . En p ime
luga , la au oma izaci´on de odo el p oceso de gene aci´on de casos. Con nues o a-
77

78 CAP´
ITULO 6. CONCLUSIONES
bajo, gene amos un iche o sm a pa i del cu´al, al ejecu a lo en Z3, ob enemos los
di e en es casos de p ueba buscados. U ilizando la API, pod emos sal a nos el paso
de c ea dicho iche o ob eniendo di ec amen e los modelos que con o man los casos
de p ueba. En segundo luga , la en aja m´as impo an e es la posibilidad de gene a
un mayo n´ume o de casos de p ueba. Has a aho a, con el iche o sm podemos da
un ´unico alo a cada una de nues as es uc u as. G acias a la API de Z3, al pode
ene acceso di ec o a los modelos p opo cionados, pod ´ıamos log a es e obje i o.
Pa a ello, hab ´ıa que analiza ales modelos pa a c ea nue as es icciones en las
que ´es os sean negados, y ol e a ejecu a despu´es consiguiendo en onces un mo-
delo di e en e al an e io . I e ando es e p oceso mien as queden combinaciones de
alo es a elegi , se pod ´ıa en onces consegui un mayo n´ume o de casos de p ueba
pa a una misma es uc u a.
Miguel Ga ido Canalejas
79
Ingl´es
A his s age, we can con i m ha he s a ed goals a he beginning o his
wo k ha e been accomplished.
As he i s main goal, we conside ed being able o ans o m a p econdi ion-
asse ion in o a se o es ic ions. Thanks o he Haskell p og am we ha e c ea ed,
displayed in he Appendix A, we can ans o m any unc ion p econdi ion, gi en
in i s in e media e ep esen a ion, o a se ies o cons ain s p ocessable by Z3, by
which o au oma ically gene a e es cases om i s sa is iabili y.
On he o he hand, he second challenge was he in es iga ion o SMT sol-
e s, Z3 in pa icula , wi h he in en o codi ying in his pla o m all he p edica es
in ol ed in he p econdi ions o some o he mos in e es ing unc ions abou he
da a s uc u es we ha e conside ed. Du ing Chap e 3, we explained he ans o -
ma ion o all he asse ions in o Z3 unc ions, showing, in addi ion, he powe o
his ool in gi ing alues o he a iables in ol ed in he aised cons ain s. The
esul s ga he ed om his in es iga ion we e dispa a e. On he one hand, while we
ha e disco e ed Z3 is e y powe ul in gi ing alues o simple ype a iables, such as
in ege s o a ays, on he o he hand i is unable o syn hesize algeb aic s uc u es
such as ees o lis s. Howe e , hanks o he p oposed s a egy o sepa a ing he
cons ain s in di e en kinds, we ha e achie ed o o e come his Z3 di icul y, so ou
sys em is qui e e ec i e.
Following his, we ha e managed o comple e he ask o gene a ing es
cases sa is ying a ce ain p econdi ion, only om i s speci ica ion.
Abou he u u e wo k, he main ex ension o he p ojec esides in using
he Z3 API o Haskell. By using i , wo ad an ages will be ob ained. Fi s , he
au oma ion o he en i e case gene a ion p ocess. Wi h ou wo k, we gene a e a sm
ile om which, when execu ing i in Z3, we ob ain he es cases we looked o wa d.
Using he API, we may skip he s ep o c ea ing such a ile, di ec ly ob aining he
models which shape he es cases. Second, he mos impo an ad an age is he
possibili y o gene a ing a la ge numbe o es cases. Up o now, wi h he sm ile
we can gi e only one alue o each o ou s uc u es. Thanks o he Z3 API, as
we ha e di ec access o he p o ided models, we could achie e his goal. In o de
o do ha , hose models should be analyzed in o de o c ea e new cons ain s
which nega e he model. Then, we will execu e again he cons ain s ob aining a
model di e en om he p e ious one. I e a ing his p ocess while i emains o
exis combina ions o he alues, a la ge numbe o es cases could be gene a ed.
T abajo Fin de G ado
80 CAP´
ITULO 6. CONCLUSIONES
Miguel Ga ido Canalejas
Ap´endice A
P og ama Haskell
A lo la go de es e ap´endice se mues a el c´odigo Haskell implemen ado
enca gado de aduci los a chi os CLIR en iche os sm . La unci´on p incipal se
encuen a en un m´odulo Main, que hace uso de una se ie de unciones de inidas en
el m´odulo As 2Sm . El m´odulo p incipal se enca ga de comp oba que los ipos de
las a iables son co ec os, lee los da os de las unciones y las decla aciones de ipos
c eados en Z3, y esc ibe el iche o de salida. El m´odulo secunda io es el enca gado
de ans o ma el ´a bol abs ac o de la unci´on dada en una secuencia de cadenas
en las que se decla en odas las a iables necesa ias y los ase os de i ados de la
p econdici´on de dicha unci´on. Adem´as, es e m´odulo es el enca gado de gene a las
dis in as es uc u as pa a cie os ipos de da os.
Dado que odo el abajo se engloba den o un p oyec o m´as g ande, el
c´odigo que se mues a a con inuaci´on queda incluido den o del p oyec o Haskell
i 2Haskell. Po ello, algunas de las llamadas a unciones que pueden encon a se, o
alguno de los m´odulos impo ados, no son p opios de es e abajo sino que co es-
ponden a abajos p e ios sob e el p oyec o global.
A.1. Main
module Main whe e
impo I 2Haskell (pa seAST, haskellcode)
impo As 2Sm ( il e Va sLis , analyzeVa s, allVa s2S ing,
pa amsCases2S ing, ob ainCasesLis , ge Asse ion, casesLis 2S ing)
impo quali ied Tex .P e yP in .Mainland as D
impo Language.Cli
impo Da a.Lis
impo quali ied Da a.Tex as T
-------------------------------------------------
--TIPOS CORRECTOS (ESTRUCTURAS ALMACENAN INT)
-------------------------------------------------
81
88 AP´
ENDICE A. PROGRAMA HASKELL
analyzeType:: Cli Type -> S ing
analyzeType x = case x o
SimpleType n -> T.unpack n
TypeVa n -> T.unpack n
CompoundType xs -> analyzeTypeLis xs
il e Va sLis :: [(S ing, S ing)] -> [(S ing, S ing)]
il e Va sLis xs = [(x,y) | (x,y)<-xs, (no (elem y ["In ", "Bool"]))]
-------------------------------------------------
--GENERADOR DE CASOS
-------------------------------------------------
gene a eCases:: [(S ing, S ing)] -> [In ] -> [[S ing]]
gene a eCases [x] [y] = case (snd x) o
"A ay" -> []
"T ee" -> [loadT ees ( s x) y]
"Ls " -> [loadLis ( s x) y]
"LLRB" -> [loadLLRBs ( s x) y]
"AVL" -> [loadAVLs ( s x) y]
gene a eCases (x:xs) (y:ys) = case (snd x) o
"A ay" -> gene a eCases xs ys
"T ee" -> (loadT ees ( s x) y):(gene a eCases xs ys)
"Ls " -> (loadLis ( s x) y):(gene a eCases xs ys)
"LLRB" -> (loadLLRBs ( s x) y):(gene a eCases xs ys)
"AVL" -> (loadAVLs ( s x) y):(gene a eCases xs ys)
combineLis s:: [[a]] -> [[a]]
combineLis s [] = [[]]
combineLis s (x:xs) = [x:y | x<-x, y<-(combineLis s xs)]
spli s:: [a] -> [([a], [a])]
spli s xs = L.zip (L.ini s xs) (L. ails xs)
---------------GENERADOR DE LISTAS---------------
loadLis :: S ing -> In -> [S ing]
loadLis x s = lis s2S ing (gene a eLis s x)
lis s2S ing:: [Ls ] -> [S ing]
lis s2S ing [] = []
lis s2S ing (x:xs) = oneLis 2S ing x:lis s2S ing xs
oneLis 2S ing:: Ls -> S ing
oneLis 2S ing x = case x o
Nil -> "nil"
Cons c l -> "(cons " ++ c ++ " " ++ oneLis 2S ing l ++ ")"
Miguel Ga ido Canalejas

A.2. AST2SMT 89
gene a eLis Aux:: S ing -> [Cha ] -> Ls
gene a eLis Aux _ [] = Nil
gene a eLis Aux n (x:xs) = Cons (n ++ [x]) (gene a eLis Aux n xs)
gene a eLis :: In -> S ing -> [Ls ]
gene a eLis n x = [gene a eLis Aux x (L. ake n [’1’..])]
--------------GENERADOR DE ´
ARBOLES---------------
loadT ees:: S ing -> In -> [S ing]
loadT ees x s = ees2S ing (gene a eT ee s x)
ees2S ing:: [T ee] -> [S ing]
ees2S ing [] = []
ees2S ing (x:xs) = oneT ee2S ing x: ees2S ing xs
oneT ee2S ing:: T ee -> S ing
oneT ee2S ing x = case x o
Lea -> "lea "
Node c l -> "(node " ++ c ++ " " ++ oneT ee2S ing l ++ " " ++
oneT ee2S ing ++ ")"
gene a eT eeAux :: S ing -> [Cha ] -> [T ee]
gene a eT eeAux _ [] = e u n Lea
gene a eT eeAux n (x:xs) = do
(le , igh ) <- spli s xs
Node <$> pu e (n++[x]) <*> gene a eT eeAux n le <*>
gene a eT eeAux n igh
gene a eT ee:: In -> S ing -> [T ee]
gene a eT ee n x = gene a eT eeAux x (L. ake n [’1’..])
----------------GENERADOR DE AVL-----------------
loadAVLs:: S ing -> In -> [S ing]
loadAVLs x s = a ls2S ing (gene a eAVL s x)
a ls2S ing:: [AVL] -> [S ing]
a ls2S ing [] = []
a ls2S ing (x:xs) = oneA l2S ing x:a ls2S ing xs
oneA l2S ing:: AVL -> S ing
oneA l2S ing x = case x o
Lea A -> "lea A"
NodeA hl ->"(nodeA"++ ++""++h++""++
oneA l2S ing l ++ " " ++ oneA l2S ing ++ ")"
T abajo Fin de G ado
90 AP´
ENDICE A. PROGRAMA HASKELL
gene a eAVLAux :: S ing -> [Cha ] -> [AVL]
gene a eAVLAux _ [] = e u n Lea A
gene a eAVLAux n (x:xs) = do
(le , igh ) <- spli s xs
NodeA <$> pu e (n++[x]) <*> pu e (n++"h"++[x]) <*> gene a eAVLAux n le <*>
gene a eAVLAux n igh
gene a eAVL:: In -> S ing -> [AVL]
gene a eAVL n x = gene a eAVLAux x (L. ake n [’1’..])
---------------GENERADOR DE LLRB-----------------
loadLLRBs:: S ing -> In -> [S ing]
loadLLRBs x s = ll bs2S ing (gene a eLLRB s x)
ll bs2S ing:: [LLRB] -> [S ing]
ll bs2S ing [] = []
ll bs2S ing (x:xs) = oneLl b2S ing x:ll bs2S ing xs
oneLl b2S ing:: LLRB -> S ing
oneLl b2S ing x = case x o
Lea L -> "lea L"
NodeL cl ->"(nodeL"++ ++""++c++""++
oneLl b2S ing l ++ " " ++ oneLl b2S ing ++ ")"
gene a eLLRBAux :: S ing -> [Cha ] -> [LLRB]
gene a eLLRBAux _ [] = e u n Lea L
gene a eLLRBAux n (x:xs) = do
(le , igh ) <- spli s xs
NodeL <$> pu e (n++[x]) <*> pu e (n++"c"++[x]) <*> gene a eLLRBAux n le <*>
gene a eLLRBAux n igh
gene a eLLRB:: In -> S ing -> [LLRB]
gene a eLLRB n x = gene a eLLRBAux x (L. ake n [’1’..])
-------------------------------------------------
--PARSING DE LOS CASOS
-------------------------------------------------
ob ainCasesLis :: TopLe elDe -> [In ] -> [[S ing]]
ob ainCasesLis x sizes = combineLis s
(gene a eCases ( il e Va sLis (analyzeVa s x)) sizes)
Miguel Ga ido Canalejas
A.2. AST2SMT 91
casesLis 2S ing:: [Asse ion] -> [[S ing]] -> [(S ing, S ing)] -> S ing
casesLis 2S ing a [x] y = "(push) n" ++ cases2S ing a x y
casesLis 2S ing a (x:xs) y = "(push) n" ++ cases2S ing a x y ++
casesLis 2S ing a xs y
cases2S ing:: [Asse ion] -> [S ing] -> [(S ing, S ing)] -> S ing
cases2S ing a [] [] = " n" ++ assLis 2S ing a ++ "(pop) n n"
cases2S ing a [] [(_, "A ay")] = " n" ++ assLis 2S ing a ++ "(pop) n n"
cases2S ing a (x:xs) (y:ys)
| (snd y) == "A ay" = "" ++ cases2S ing a (x:xs) ys
| o he wise = "(asse (= " ++ s y ++ " " ++ x ++ ")) n" ++
cases2S ing a xs ys
-------------------------------------------------
--PARSING DE LOS PAR´
AMETROS DE LOS CASOS
-------------------------------------------------
pa amsCases2S ing:: [(S ing, S ing)] -> [In ] -> S ing
pa amsCases2S ing [x] [y] = case (snd x) o
"A ay" -> sizeA 2S ing ( s x) y ++ pa amsA 2S ing ( s x) (L. ake y [’0’..])
"Ls " -> pa amsLis 2S ing ( s x) (L. ake y [’1’..])
"T ee" -> pa amsT ee2S ing ( s x) (L. ake y [’1’..])
"LLRB" -> pa amsLLRB2S ing ( s x) (L. ake y [’1’..])
"AVL" -> pa amsAVL2S ing ( s x) (L. ake y [’1’..])
pa amsCases2S ing (x:xs) (y:ys) = case (snd x) o
"A ay" -> sizeA 2S ing ( s x) y ++ pa amsCases2S ing xs ys
"Ls " -> pa amsLis 2S ing ( s x) (L. ake y [’1’..]) ++ pa amsCases2S ing xs ys
"T ee" -> pa amsT ee2S ing ( s x) (L. ake y [’1’..]) ++ pa amsCases2S ing xs ys
"LLRB" -> pa amsLLRB2S ing ( s x) (L. ake y [’1’..]) ++ pa amsCases2S ing xs ys
"AVL" -> pa amsAVL2S ing ( s x) (L. ake y [’1’..]) ++ pa amsCases2S ing xs ys
sizeA 2S ing:: S ing -> In -> S ing
sizeA 2S ing n x = "(asse (= (second " ++ n ++ ") " ++ (show x) ++ ")) n n"
pa amsA 2S ing:: S ing -> [Cha ] -> S ing
pa amsA 2S ing _ [] = " n"
pa amsA 2S ing n (x:xs) =
"(asse (> (selec ( i s " ++ n ++ ") " ++ [x] ++ ") -5)) n" ++
"(asse (< (selec ( i s " ++ n ++ ") " ++ [x] ++ ") 5)) n" ++
pa amsA 2S ing n xs
T abajo Fin de G ado
92 AP´
ENDICE A. PROGRAMA HASKELL
pa amsLis 2S ing:: S ing -> [Cha ] -> S ing
pa amsLis 2S ing _ [] = " n"
pa amsLis 2S ing n (x:xs) = "(decla e-cons " ++ n ++ [x] ++ " In ) n" ++
"(asse (> " ++ n ++ [x] ++ " -5)) n" ++
"(asse (< " ++ n ++ [x] ++ " 5)) n" ++
pa amsLis 2S ing n xs
pa amsT ee2S ing:: S ing -> [Cha ] -> S ing
pa amsT ee2S ing _ [] = " n"
pa amsT ee2S ing n (x:xs) = "(decla e-cons " ++ n ++ [x] ++ " In ) n" ++
"(asse (> " ++ n ++ [x] ++ " -5)) n" ++
"(asse (< " ++ n ++ [x] ++ " 5)) n" ++
pa amsT ee2S ing n xs
pa amsLLRB2S ing:: S ing -> [Cha ] -> S ing
pa amsLLRB2S ing n xs = pa amsLLRBVal2S ing n xs ++ pa amsLLRBColo 2S ing n xs
pa amsLLRBVal2S ing:: S ing -> [Cha ] -> S ing
pa amsLLRBVal2S ing n [x] = "(decla e-cons " ++ n ++ [x] ++ " In ) n" ++
"(asse (> " ++ n ++ [x] ++ " -5)) n" ++
"(asse (< " ++ n ++ [x] ++ " 5)) n"
pa amsLLRBVal2S ing n (x:xs) = "(decla e-cons " ++ n ++ [x] ++ " In ) n" ++
"(asse (> " ++ n ++ [x] ++ " -5)) n" ++
"(asse (< " ++ n ++ [x] ++ " 5)) n" ++
pa amsLLRBVal2S ing n xs
pa amsLLRBColo 2S ing:: S ing -> [Cha ] -> S ing
pa amsLLRBColo 2S ing n [x] = "(decla e-cons " ++ n ++ "c" ++ [x] ++ " Colo ) n"
pa amsLLRBColo 2S ing n (x:xs) = "(decla e-cons " ++ n ++ "c" ++ [x] ++
" Colo ) n" ++ pa amsLLRBColo 2S ing n xs
pa amsAVL2S ing:: S ing -> [Cha ] -> S ing
pa amsAVL2S ing n xs = pa amsAVLVal2S ing n xs ++ pa amsAVLHeigh 2S ing n xs
pa amsAVLVal2S ing:: S ing -> [Cha ] -> S ing
pa amsAVLVal2S ing n [x] = "(decla e-cons " ++ n ++ [x] ++ " In ) n" ++
"(asse (> " ++ n ++ [x] ++ " -5)) n" ++
"(asse (< " ++ n ++ [x] ++ " 5)) n"
pa amsAVLVal2S ing n (x:xs) = "(decla e-cons " ++ n ++ [x] ++ " In ) n" ++
"(asse (> " ++ n ++ [x] ++ " -5)) n" ++
"(asse (< " ++ n ++ [x] ++ " 5)) n" ++
pa amsAVLVal2S ing n xs
pa amsAVLHeigh 2S ing:: S ing -> [Cha ] -> S ing
pa amsAVLHeigh 2S ing n [x] = "(decla e-cons " ++ n ++ "h" ++ [x] ++ " In ) n"
pa amsAVLHeigh 2S ing n (x:xs) = "(decla e-cons " ++ n ++ "h" ++ [x] ++
" In ) n" ++ pa amsAVLHeigh 2S ing n xs
Miguel Ga ido Canalejas
A.2. AST2SMT 93
-------------------------------------------------
--PARSING DE LAS VARIABLES
-------------------------------------------------
allVa s2S ing:: TopLe elDe -> S ing
allVa s2S ing (TopFunDe _ xs _ _ _) = a Lis 2S ing xs
a Lis 2S ing:: [TypedVa ] -> S ing
a Lis 2S ing [] = " n"
a Lis 2S ing (x:xs) = a 2S ing x ++ a Lis 2S ing xs
a 2S ing:: TypedVa -> S ing
a 2S ing (TypedVa n x) = "(decla e-cons " ++ n ++ " " ++ ype2S ing x ++ ") n"
ypesLis 2S ing:: [Cli Type] -> S ing
ypesLis 2S ing [] = ""
ypesLis 2S ing (x:xs) = ype2S ing x ++ " " ++ ypesLis 2S ing xs
ype2S ing:: Cli Type -> S ing
ype2S ing (SimpleType n)
| =="A ay" = "A "
| o he wise =
whe e = T.unpack n
ype2S ing (TypeVa n) = T.unpack n
ype2S ing (CompoundType xs) = "(" ++ ypesLis 2S ing xs ++ ")"
T abajo Fin de G ado

94 AP´
ENDICE A. PROGRAMA HASKELL
Miguel Ga ido Canalejas
Ap´endice B
Resul ados de Ejecuci´on
Cuando ejecu amos nues o p og ama Haskell sob e un iche o CLIR, ob e-
nemos como salida un iche o sm con odas las es icciones necesa ias, que es el que
pasamos a Z3 pa a ob ene as´ı los di e en es modelos. En es e ap´endice se mues a
al iche o, a in de pode comp oba que la aducci´on que ealiza nues o p og ama
es co ec a. La cabece a de es e iche o es muy ex ensa y ´unicamen e cons a de las
decla aciones de los ipos y las unciones de que se explica on en el Cap´ı ulo 3. Po
ello, aqu´ı lo ´unico que se mues a es la pa e del iche o es ic amen e pe enecien e
a la decla aci´on de a iables y la c eaci´on de es icciones a pa i del iche o CLIR.
El a chi o mos ado co esponde a la aducci´on de la unci´on inse LLRB pa a
´a boles de ca dinal es. Adem´as, al ejecu a Z3 los modelos se uelcan sob e un
iche o x desde el que pode analiza los esul ados. Se mues a ambi´en en es e
ap´endice dicho iche o pa a la misma unci´on an e io .
B.1. Fiche o Sm
(decla e-cons (LLRB In ))
(decla e-cons x In )
(decla e-cons 1 In )
(asse (> 1 -5))
(asse (< 1 5))
(decla e-cons 2 In )
(asse (> 2 -5))
(asse (< 2 5))
(decla e-cons 3 In )
(asse (> 3 -5))
(asse (< 3 5))
(decla e-cons c1 Colo )
(decla e-cons c2 Colo )
(decla e-cons c3 Colo )
95
96 AP´
ENDICE B. RESULTADOS DE EJECUCI´
ON
(push)
(asse (= (nodeL 1 c1 lea L (nodeL 2 c2 lea L (nodeL 3 c3 lea L lea L)))))
(asse (isLLRB ))
(check-sa )
(ge -model)
(pop)
(push)
(asse (= (nodeL 1 c1 lea L (nodeL 2 c2 (nodeL 3 c3 lea L lea L) lea L))))
(asse (isLLRB ))
(check-sa )
(ge -model)
(pop)
(push)
(asse (= (nodeL 1 c1 (nodeL 2 c2 lea L lea L) (nodeL 3 c3 lea L lea L))))
(asse (isLLRB ))
(check-sa )
(ge -model)
(pop)
(push)
(asse (= (nodeL 1 c1 (nodeL 2 c2 lea L (nodeL 3 c3 lea L lea L)) lea L)))
(asse (isLLRB ))
(check-sa )
(ge -model)
(pop)
(push)
(asse (= (nodeL 1 c1 (nodeL 2 c2 (nodeL 3 c3 lea L lea L) lea L) lea L)))
(asse (isLLRB ))
(check-sa )
(ge -model)
(pop)
Miguel Ga ido Canalejas
B.2. FICHERO TXT 97
B.2. Fiche o Tx
unsa
(e o "line 477 column 10: model is no a ailable")
unsa
(e o "line 486 column 10: model is no a ailable")
sa
(model
(de ine- un c1 () Colo
Neg o)
(de ine- un () (LLRB In )
(nodeL 1 Neg o (nodeL 0 Neg o lea L lea L) (nodeL 2 Neg o lea L lea L)))
(de ine- un 3 () In
2)
(de ine- un 2 () In
0)
(de ine- un c2 () Colo
Neg o)
(de ine- un 1 () In
1)
(de ine- un c3 () Colo
Neg o)
(de ine- un minTL ((x!0 (LLRB In ))) In
(i e (= x!0 lea L) 2000
(le ((a!1 (+ (minTL (izq x!0)) (* (- 1) (minTL (de x!0))))))
(le ((a!2 (i e (>= a!1 0) (minTL (de x!0)) (minTL (izq x!0)))))
(i e (>= (+ ( al x!0) (* (- 1) a!2)) 0) a!2 ( al x!0))))))
(de ine- un maxT ((x!0 (T ee In ))) In
(i e (= x!0 lea ) (- 2000)
(le ((a!1 (+ (maxT (izq x!0)) (* (- 1) (maxT (de x!0))))))
(le ((a!2 (i e (<= a!1 0) (maxT (de x!0)) (maxT (izq x!0)))))
(i e (<= (+ ( alue x!0) (* (- 1) a!2)) 0) a!2 ( alue x!0))))))
(de ine- un mul ise A ((x!0 In ) (x!1 (A ay In In )) (x!2 In )) (A ay In
In )
(i e (= x!0 x!2)
((as cons (A ay In In )) 0)
((_ map (+ (In In ) In ))
(mul ise A (+ 1 x!0) x!1 x!2)
(s o e ((as cons (A ay In In )) 0) (selec x!1 x!0) 1))))
(de ine- un ca dA ((x!0 (AVL In ))) In
(i e (= x!0 lea A) 0
(+ 1 (ca dA (izq x!0)) (ca dA (de x!0)))))
(de ine- un k!0 ((x!0 In )) In
5)
(de ine- un k!29 ((x!0 (LLRB In ))) (LLRB In )
(i e (= x!0 (nodeL 0 Neg o lea L lea L)) (nodeL 0 Neg o lea L lea L)
lea L))
(de ine- un minHeigh ((x!0 (T ee In ))) In
T abajo Fin de G ado
104 BIBLIOGRAF´
IA
Selec ed Pape s, olume 9527 o Lec u e No es in Compu e Science, pages 227–
243. Sp inge , 2015.
Miguel Ga ido Canalejas