Ve i icación de algo i mos sob e segmen os de un
ec o u ilizando módulos abs ac os en Da ny
Ve i ica ion o algo i hms on a ay slices using
abs ac modules in Da ny
T abajo de Fin de G ado
Cu so 2023–2024
Au o
Pablo Ma ín Viñuelas
Di ec o a
Cla a Ma ía Segu a Díaz
Doble G ado en Ma emá icas e Ingenie ía In o má ica
Facul ad de In o má ica
Uni e sidad Complu ense de Mad id
Ve i icación de algo i mos sob e segmen os
de un ec o u ilizando módulos abs ac os
en Da ny
Ve i ica ion o algo i hms on a ay slices
using abs ac modules in Da ny
T abajo de Fin de G ado en Ingenie ía In o má ica
Au o
Pablo Ma ín Viñuelas
Di ec o
Cla a Ma ía Segu a Díaz
Con oca o ia: Junio 2024
Doble G ado en Ma emá icas e Ingenie ía In o má ica
Facul ad de In o má ica
Uni e sidad Complu ense de Mad id
26 de mayo de 2024
Resumen
Ve i icación de algo i mos sob e segmen os de un ec-
o u ilizando módulos abs ac os en Da ny
La e i icación o mal de p og amas pe mi e exp esa y comp oba las p opie-
dades que cumplen los p og amas. El obje i o de es e p oyec o es el de e i ica
algo i mos que compu an in o mación sob e los segmen os de un ec o , como po
ejemplo el segmen o más la go que cumple una p opiedad o el núme o de segmen os
que cumple una p opiedad.
En p ime luga , se in oduci á la he amien a Da ny, un lenguaje de p og ama-
ción que u iliza un esolu o SMT pa a comp oba las condiciones de e i icación
necesa ias in oducidas po el usua io.
En segundo luga , se lle a á a cabo una explicación de los algo i mos con los que
amos a abaja y algunos ejemplos conc e os de su aplicación. Pos e io men e,
se modeliza án es e ipo de p oblemas en Da ny, pa a pode así lle a a cabo la
implemen ación del algo i mo en la he amien a, con el in de inalmen e e i ica
que cumple las p opiedades que espe amos de las soluciones. Se a a á de p esen a
cada p oblema con di e en es ni eles de abs acción, es deci , pa a cada p oblema
se p esen a án di e en es soluciones dependiendo del ipo de p opiedades que se
es én comp obando sob e los segmen os. De es a o ma, pa a de e minados casos
ob end emos soluciones más e icien es.
Palab as cla e
e i icación, Da ny, algo i mia, e i icación asis ida.

Abs ac
Ve i ica ion o algo i hms on a ay slices using ab-
s ac modules in Da ny
Fo mal e i ica ion echniques allow us o exp ess and check he p ope ies ha
p og ams mee . The pu pose o his p ojec is o e i y algo i hms ha compu e
in o ma ion conce ning he segmen s o a ec o , such as he longes segmen ha
holds a p ope y o he numbe o segmen s ha hold a ce ain p ope y.
Fi s ly, we in oduce he ool we ha e used, Da ny. I is a p og amming language
ha uses a SMT sol e o check whe he o no he e i ica ion condi ions speci ied
by he use a e ul illed.
Secondly, we will deepen in o he algo i hms we ha e s udied and some conc e e
examples. La e we will model hose p oblems using Da ny so ha we a e able o
e i y ha he algo i hm implemen a ion e i ies he p ope ies we expec . We will
p esen each kind o p oblem wi h di e en le els o abs ac ion. To each kind o
p oblem we will p esen di e en solu ions depending on he ype o p ope y being
checked on segmen s. This way, we will ob ain mo e e icien solu ions o some
speci ic cases.
Keywo ds
e i ica ion, Da ny, algo i hmics, assis ed e i ica ion
ii
Índice
1. In oducción 1
1.1. Obje i os ................................. 1
1.2. Plande abajo.............................. 2
2. Da ny 5
2.1. Especi icación e implemen ación . . . . . . . . . . . . . . . . . . . . . 5
2.1.1. Implemen ación y mé odos . . . . . . . . . . . . . . . . . . . . 7
2.1.2. Especi icación y unciones . . . . . . . . . . . . . . . . . . . . 8
2.1.3. TiposenDa ny .......................... 9
2.1.4. Módulos.............................. 10
3. Algo i mos pa a el p ocesamien o de segmen os 15
3.1. De iniciones y concep os . . . . . . . . . . . . . . . . . . . . . . . . . 15
3.2. Esquema gene al de algo i mos i e a i os . . . . . . . . . . . . . . . . 16
3.3. Tipos de p oblemas con emplados . . . . . . . . . . . . . . . . . . . . 17
3.3.1. P oblemas de segmen os de longi ud máxima . . . . . . . . . . 17
3.3.2. P oblemas de con a segmen os . . . . . . . . . . . . . . . . . 18
3.4. O osp oblemas.............................. 20
4. P oblemas de segmen os de longi ud máxima 21
4.1. Modelización del p oblema . . . . . . . . . . . . . . . . . . . . . . . . 22
4.2. Demos ación de la co ección . . . . . . . . . . . . . . . . . . . . . . 26
4.3. Abs acción y conc eción sob e los p oblemas . . . . . . . . . . . . . . 27
4.3.1. P opiedades ce adas po la izquie da . . . . . . . . . . . . . . 28
4.3.2. P opiedades uni e sales sob e elemen os . . . . . . . . . . . . 29
ix

Cap´
ı ulo 2
Da ny
Da ny es una he amien a diseñada pa a la e i icación de so wa e median e
el pa adigma de “Co ec o po Cons ucción”. Es á compues o po un lenguaje de
p og amación y mecanismos que pe mi en la especi icación de p og amas. Da ny, [4]
es á diseñado pa a pe mi i pa alelamen e el desa ollo de código y una demos ación
de su co ección. Da ny conside a que un p og ama es co ec o si es e e mina y
sa is ace la especi icación p opo cionada.
Pa a alcanza es e obje i o, el usua io debe á p opo ciona una especi icación
sob e el compo amien o que se espe a del p og ama. Es e p oceso se lle a a cabo
median e el uso de p econdiciones y pos condiciones, que son p opiedades que de-
be án se e i icadas an es y después de la ejecución de cada uno de los mé odos,
unciones y lemas.
Da ny ue c eado po Rus an Leino pa a Mic oso Resea ch, y se ha u ilizado
en di e en es p oyec os, como po ejemplo pa a la e i icación del AWS Enc yp ion
SDK, [6] y pa a la especi icación y e i icación de la ed E h2.0, [3]. El lenguaje
combina ideas de los pa adigmas impe a i o y uncional, y puede se compilado a
o os lenguajes como Ja a, C#, Ja aSc ip o Py hon. Pa a comp oba las demos-
aciones, Da ny hace uso del demos ado au omá ico de eo emas Z3 a a és del
lenguaje in e medio Boogie.
En es e capí ulo se in oducen algunos concep os impo an es de Da ny. Se á
de especial impo ancia in oduci los mecanismos que nos p opo ciona Da ny pa a
lle a a cabo la especi icación y e i icación. También se p esen a án concep os como
módulos o ipos que se án u ilizados ambién en nues o p oyec o. Se ha omado
como e e encia el capí ulo homólogo de Paula Pas o Pé ez en su T abajo Fin de
Mas e Ve i ica ion o G eedy Algo i hms in Da ny [9].
2.1. Especi icación e implemen ación
Dado que el obje i o de Da ny es el de lle a a cabo de mane a pa alela la
especi icación y la implemen ación de los p og amas, es impo an e man ene una
5
6Capí ulo 2. Da ny
sepa ación en e es os dos mundos pa a así consegui un código más legible y sencillo
de comp ende .
Aquí juega un papel impo an e la combinación que encon amos en Da ny de
los pa adigmas impe a i o y uncional. Con el p ime o es con el que amos a im-
plemen a nues os p og amas, haciendo uso de mé odos y de es uc u as de da os,
como los a ay, que con emplan los e ec os la e ales, mien as que con el segundo
lle a emos a cabo la especi icación median e unciones y es uc u as de da os, como
las secuencias, que no pe mi en los e ec os la e ales.
Pa a pode conec a ambos mundos, nos alemos de las cláusulas equi es yen-
su es que ep esen an las ya mencionadas p econdiciones y pos condiciones. Es as
cláusulas se esc iben debajo de la cabece a de los mé odos, unciones y lemas. Da ny
asume que la p econdición siemp e se cumple al inicio de la ejecución del mé odo,
unción o lema. Es po es o que si a amos de hace una llamada a un mé odo (o
unción o lema), Da ny comp oba á si se cumple la p econdición an es de ejecu a el
cue po, y de ol e á e o en caso con a io. Po o o lado, las clausulas ensu es espe-
ci ican una p opiedad que ha de cumpli se al inaliza el mé odo (o unción o lema).
La ausencia de p econdiciones o pos condiciones se co esponde con las cláusulas
equi es ue yensu es ue, espec i amen e. La p ime a de ellas es i ialmen e
cie a, mien as que la segunda simplemen e nos asegu a la e minación.
Nues os mé odos se án especi icados median e unciones ecu si as que u ili-
za emos en las p econdiciones y pos condiciones de los mismos, y con end án la
implemen ación de nues o p og ama. Pa a pode e i ica que los mé odos alcan-
zan la pos condición pa iendo de la p econdición, end emos que p oba una se ie
de p opiedades sob e las unciones que hemos de inido, es e p oceso se lle a a cabo
median e los lemas y ase os. Como esul ado de es e p oceso ob enemos un mé odo
e i icado en el que el usua io pod á con ia , ya que los mecanismos de Da ny le
asegu an que si la en ada cumple la p econdición en onces a la salida del mé odo se
alcanza la pos condición, sin necesidad de que el usua io comp enda la implemen-
ación ni la demos ación de la co ección de la misma.
Has a aho a hemos desc i o como podemos modela que el p og ama al e mina
cumple con lo que espe amos que haga, pe o no podemos asegu a que e mine. Con
es e in Da ny nos p opo ciona las clausulas dec eases. La clausula si e pa a asegu a
la e minación. Todas las unciones, mé odos y bucles iene asociada una cláusula
de es e ipo, aunque no apa ezca de mane a explíci a, no malmen e Da ny es capaz
de in e i las au omá icamen e, pe o en ocasiones debemos indica las noso os. Una
clausula dec eases es á de inida po una exp esión, llamada medida de e minación,
que es no nega i a y que en cada nue a i e ación o llamada ecu si a, su alo
dec ece.
En las siguien es subsecciones, nos cen a emos en es udia cómo lle a a cabo
la especi icación e implemen ación de nues os p og amas, desc ibiendo los mecanis-
mos que nos p opo ciona Da ny pa a lle a a cabo es a a ea. Finalmen e, ambién
habla emos de los módulos y los ipos que nos p opo ciona Da ny.
2.1. Especi icación e implemen ación 7
me hod T i p l e ( x :in ) e u ns ( :in ) {
a y:= 2∗x ;
:= x + y ;
}
Figu a 2.1: Ejemplo de mé odo T iple en Da ny
2.1.1. Implemen ación y mé odos
El obje i o de la implemen ación es el de gene a un p og ama que cumpla con
las expec a i as del modelado. Con es e in se p esen an los mé odos. Un mé odo
es una sucesión de decla aciones que lle a a cabo una se ie de cambios en el es ado
de nues a máquina. Un ejemplo de mé odo se ía el que apa ece en la Figu a 2.1,
enca gado de calcula el iple de un alo . Es e mé odo ecibe un pa áme o de
en ada xde ipo en e o y de uel e un pa áme o de salida , que ambién es en e o.
El cue po del mé odo es una se ie de sen encias que en su conjun o con o ma la
implemen ación del mé odo. Los pa áme os de salida ac úan como a iables locales.
Los pa áme os de en ada pueden se leídos pe o no pueden cambia su alo .
El cue po de un mé odo puede con ene di e en es sen encias, como bucles o
llamadas a o os mé odos o lemas. Como puede e se en la Figu a 2.1 no es necesa io
decla a el ipo de una a iable cuando la decla amos, ya que Da ny es capaz de
in e i lo. Pa a de ol e un alo desde un mé odo, debemos asigná selo al pa áme o
de salida.
Una sen encia especial es el while. La e i icación de bucles en Da ny necesi a
sabe qué p opiedades se man ienen a lo la go de las i e aciones del bucle, el in a-
ian e, pa a pode demos a que se cumplen al e mina es e. También necesi amos
demos a que nues o bucle e mina, pa a ello u ilizamos una clausula dec ease,
aunque no malmen e Da ny es capaz de e i ica lo de o ma au má ica.
El in a ian e de un bucle es una p opiedad que es cie a a la en ada y salida
del bucle, así como en el momen o de comp oba la condición de salida del bucle en
cada una de las i e aciones. Pa a exp esa nues o in a ian e pa a un cie o bucle,
u ilizamos la clausula in a ian . Se mues a un ejemplo en la Figu a 2.2. Se a a
de un p og ama que calcula el cocien e y el es o de di idi 191 en e 7 a base de
es a el di iso al di idendo has a que el di idendo se uel e meno que el di iso .
El in a ian e exp esa que la elación 0≤y∧7∗x+y= 191 se man iene a lo la go
de la ejecución del bucle.
En ocasiones, Da ny no pod á e i ica au omá icamen e la co ección de es as
clausulas. Es po eso que u ilizamos ase os, que hacemos explíci os median e la
clausula asse . Es as exp esiones han de se cie as en cualquie momen o en que
la ejecución alcanza el pun o en el que es án de inidas. Pueden se u ilizadas an o
en mé odos como en lemas.
Cuando Da ny no es capaz de demos a la co ección de un ase o que sabemos
es cie o, u ilizamos lemas pa a ayuda a Da ny a conclui la p opiedad deseada. Un
8Capí ulo 2. Da ny
a x , y := 0 , 191;
while 7≤y
in a ian 0≤y∧7∗x+y=191
dec eases y
{
y:= y−7;
x:= x + 1 ;
}
a s s e x=191 / 7 ∧y=191 % 7;
Figu a 2.2: Bucle pa a el cálculo del cocien e y módulo de 191 espec o a 7
lema es una a i mación ma emá ica que iene acompañada de su demos ación. En
Da ny, un lema es muy pa ecido a un mé odo: iene un nomb e, podemos añadi le
pa áme os, iene p econdición y pos condición y podemos llama lo. La di e encia
con los mé odos es que los lemas no son conside ados po el compilado , solo se
ienen en cuen a du an e la e i icación. Pa a decla a un lema p ocedemos de la
misma o ma que con los mé odos, pe o cambiando la palab a me hod po lemma.
2.1.2. Especi icación y unciones
El obje i o de la especi icación es el de desc ibi el compo amien o de los p o-
g amas que amos a implemen a . Es a especi icación se lle a a cabo median e las
ya explicadas p econdiciones y pos condiciones, y ambién a a és de las unciones.
Una unción deno a un alo compu ado dados unos a gumen os. La p opiedad
que dis ingue a las unciones es que son de e minis as, es deci , que no p esen an
e ec os cola e ales. Un ejemplo de una decla ación de unción en Da ny se ía la que
apa ece en el siguien e ex ac o de código:
unc ion A e age ( a :in , b :in ):in {
( a + b ) / 2
}
Nó ese que, mien as un mé odo es decla ado con una se ie de pa áme os de
salida, en su luga una unción decla a el esul ado en o ma de ipo, y mien as
que el cue po del mé odo consis e en una se ie de ins ucciones, el cue po de una
unción es una exp esión.
A su ez, las unciones pueden se u ilizadas en las exp esiones, de mane a que
podemos esc ibi las pos condiciones como en el mé odo siguien e:
me hod T i p l e ( x :in ) e u ns ( :in )
ensu es A e age ( , 3 ∗x ) =3∗x
El código an e io saca a eluci o a di e encia impo an e en e mé odos y
unciones en Da ny. Mien as que los mé odos son opacos, las unciones son ans-
pa en es. Es o quie e deci que Da ny no en iende una unción solo como la pa eja
2.1. Especi icación e implemen ación 9
de su p econdición y pos condición, sino que ambién conoce su cue po a la ho a de
azona sob e sus p opiedades.
Cuando azonamos sob e un p og ama, es bas an e común necesi a más in o -
mación de la que necesi a el compilado . Po es a azón, una decla ación, a iable,
unción, e c. que se u iliza solo en el con ex o de la e i icación, se denomina ghos .
El e i icado iene en cuen a a los ghos , pe o no así el compilado , que los elimina
cuando gene a el código compilado.
Noso os u iliza emos unciones ghos o an asma pa a modela el compo amien-
o de nues o p og ama, es as unciones desapa ece án du an e la compilación pe o
nos se i án pa a azona sob e el compo amien o que se espe a de los mé odos.
Un ejemplo de es a o ma de azona apa ece en el siguien e ex ac o de código:
ghos u n c i o n ibonacci(n :na ):na
dec eases n
{
i ( n =0∨n=1) hen n
else ibonacci(n −1) + i b o n a c c i ( n −2)
}
me hod m_ ibonacci(n :in ) e u ns ( :in )
e q u i e s n≥0
ensu es = i b o n a c c i ( n)
2.1.3. Tipos en Da ny
Los ipos en Da ny se clasi ican en alo y e e encia. Los p ime o son aquellos
que es án de inidos po ipos escala es básicos (in ,na ,bool...) y ag upaciones de
los an e io es (seq,se ,mul ise ...). Es os ipos son inmu ables.
Pa a cualquie ipo T, cada uno de los alo es de ipo se <T> es un conjun o
ini o de alo es del ipo T. Un conjun o es á o mado po una colección de elemen os
del mismo ipo, sin epe iciones y sin un o den conc e o. El conjun o acío se exp esa
con {}. Da ny p esen a una no ación al e na i a pa a de ini conjun os, u ilizando
se comp ehension. La siguien e no ación: se x: T | p(x) :: (x) nos de uel e el
conjun o de los elemen os (x) ales que se cumple p(x). La no ación |s| nos de uel e
el amaño del conjun o. Mos amos a con inuación algunos ejemplos:
a s:= {1 , 2 , 3 , 4} ;
a := {2 , 3 ,4 , 1};
a s s e s= ;
El ipo que amos a u iliza pa a ep esen a segmen os en nues as unciones y
lemas es la secuencia (seq<T>) donde T ep esen a el ipo de los elemen os con eni-
dos en los segmen os con los que es amos abajando. En es e caso los elemen os sí
es án o denados, al ene odos ellos un índice asociado. Podemos ex ae elemen os
de la secuencia u ilizando índices (s[i]) y co es (s[lo..hi]), en el p ime caso se
de uel e el elemen o en cues ión, mien as que el segundo se ob iene una nue a se-
cuencia o mada po el esul ado de oma los p ime os hi elemen os y desecha los lo

10 Capí ulo 2. Da ny
p ime os. La longi ud de una secuencia ( )la podemos ob ene median e la no ación
| |. Podemos obse a algunos ejemplos de es e ipo de da os a con inuación:
a s:= [ 1 , 2 , 3 , 4 ] ;
a s s e s[2..4] =[3 , 4 ] ;
a s s e |s| =4 ;
Exis en o os ipos inmu ables como los mul ise ,s ing ymap, pe o no amos a
p o undiza en ellos ya que no los amos a u iliza en nues o abajo.
Además de los ipos alo que hemos explicado, Da ny ambién p esen a los ipos
e e encia. En es e g upo se encuad an las class y los a ay. Es os ipos sí son
mu ables. En es e abajo solo se han u ilizado a ay, po lo que nos cen a emos en
explica es e ipo.
Los a ay de Da ny son de amaño ijo y se almacenan en el heap. Pa a ob ene
la longi ud de un a ay (a) dado, podemos u iliza la no ación a.Leng h que nos de-
uel e la longi ud en o ma de núme o na u al. De mane a análoga a las secuencias,
podemos u iliza índices pa a accede a los elemen os del a ay. De mane a adicio-
nal, podemos con e i los a ay a secuencias, u ilizando la no ación que apa ece en
el siguien e código:
a a:= new i n [ 3 ]
a s s e a . Leng h =3 ;
a [ 0 ] , a [ 1 ] , a [ 2 ] := 6 , 28 , 496;
a s:= a[1..3]
a s s e s=[ 28 , 496]
Si no especi icamos los índices en la an e io no ación, es deci a[..], la secuencia
esul an e con end á a odo el a ay.
Además de lo an e io , Da ny nos pe mi e ep esen a pa es de elemen os, no
necesa iamen e del mismo ipo. Si quisié amos ag upa dos elemen os, el p ime o
( ) de ipo Ty el segundo (u) de ipo U, podemos ob ene un elemen o de ipo
(T, U) median e el cons uc o ( , u). Pa a accede al p ime elemen o de un pa p,
u ilizamos el des uc o p.0, e igual pa a el segundo, u iliza emos p.1.
Como apun e inal espec o a los ipos, debemos habla de la es uc u a de
da os que hemos u ilizado pa a ep esen a los segmen os. En los mé odos, el ec o
iene dado po un a ay del ipo con el que se es é abajando, mien as que en las
unciones y lemas nos alemos de secuencias. Es a decisión se oma con el obje i o
de man ene sepa adas la implemen ación y la especi icación.
2.1.4. Módulos
La abs acción y la ocul ación de in o mación son aspec os necesa ios en un
buen diseño de p og amas, ya que nos pe mi en maneja de o ma más sencilla
las complejas elaciones en e las dis in as pa es de nues o p og ama. Los módulos
2.1. Especi icación e implemen ación 11
nos pe mi en ag upa ipos, mé odos, unciones y o os módulos, que gua dan cie a
elación en e ellos.
Noso os amos a u iliza dos ipos de sen encias sob e módulos en nues o a-
bajo: la de inición y la impo ación.
Cuando de inimos nue os módulos, u ilizamos la palab a ese ada module, se-
guida del nomb e del módulo y el cue po del mismo. En el cue po podemos inclui
mé odos, unciones, lemas, o os módulos, e c. Todos los elemen os de inidos den o
de un módulo es án disponibles pa a su uso po o os elemen os del módulo, pe o
no así pa a aquellos ue a del módulo. Si que emos impo a los elemen os de o o
módulo, podemos hace lo median e la palab a ese ada impo seguida del nomb e
del módulo. Si que emos e i a ene que hace e e encia a los elemen os del o o
módulo con el nomb e del módulo p ecediendo el del elemen o, podemos u iliza
impo opened, pe o debemos e i a con lic os en e ambos módulos.
De i al impo ancia pa a nues o p oyec o son los módulos abs ac os y el e ina-
mien o de los mismos. Los p ime os son módulos que p esen an mé odos, unciones o
lemas sin implemen a y se á en los módulos que e ina án a es os donde implemen-
a emos es os mé odos, unciones o lemas. Los módulos abs ac os no son compilados
y se decla an p ecediendo la de inición del módulo con la palab a ese ada abs ac .
Un módulo que e ina a o o es un módulo que incluye odas las p opiedades, de-
iniciones, mé odos o lemas del p ime o, añadiendo elemen os adicionales pa a una
mayo pa icula ización. Podemos obse a ejemplos de lo explicado en las Figu as
2.3 y 2.4. Es os ejemplos se han ex aído del abajo in de más e : Ve i ica ion o
g eedy algo i hms in Da ny [9] y ep esen an la es uc u a ma emá ica de g upo y
de g upo adi i o de en e os, es e segundo como e inamien o del p ime o.
12 Capí ulo 2. Da ny
a b s a c module G oup {
ype G
unc ion P oduc (x :G, y :G) :G
lemma Associa i i y(x :G, y :G, z :G)
ensu es P oduc (x , P oduc (y , z)) =P oduc ( P oduc ( x , y ) , z )
unc ion I d e n i y ( ) :G
lemma Iden i yIsNeu al(x :G)
ensu es P oduc ( x , I d e n i y ( ) ) =x
ensu es P oduc ( I d e n i y ( ) , x ) =x
unc ion In e se(x :G) :G
lemma P oduc In e se(x :G)
ensu es P oduc ( x , I n e s e ( x )) =I d e n i y ( )
ensu es P oduc ( I n e s e ( x ) , x ) =I d e n i y ()
lemma S i m p l i y L e ( a :G, b :G, c :G)
e q u i e s P oduc ( a , b ) =P oduc ( a , c )
ensu es b=c
{
calc {
P oduc ( a , b ) =P oduc ( a , c )
=⇒
P oduc ( I n e s e ( a ) , P oduc ( a , b ))
=P oduc ( I n e s e ( a ) , P oduc ( a , c ) ) ;
=⇒{ A s s o c i a i i y ( I n e s e ( a ) , a , b ) ; A s s o c i a i i y ( I n e s e ( a ) , a , c ) ; }
P oduc ( P oduc ( I n e s e ( a ) , a ) , b )
=P oduc ( P oduc ( I n e s e ( a ) , a ) , c ) ;
=⇒{ P o d u c I n e s e ( a ) ; }
P oduc ( I d e n i y ( ) , b ) =P oduc ( I d e n i y ( ) , c ) ;
=⇒{ Iden i yIsNue al(b); Iden i yIsNeu al(c); }
b=ca ;
}
}
}
Figu a 2.3: Módulo abs ac o que ep esen a la es uc u a de g upo
2.1. Especi icación e implemen ación 13
module Addi i eIn e ines G oup {
ype G = in
unc ion P oduc (x:G, y :G) :G {
x+y
}
lemma Associa i i y(x :G, y :G, z :G)
ensu es P oduc (x , P oduc (y , z)) =P oduc ( P oduc ( x , y ) , z )
{}
unc ion I d e n i y ( ) :G {
0
}
lemma Iden i yIsNeu al(x :G)
ensu es P oduc ( c , I d e n i y ( )) =x
ensu es P oduc ( I d e n i y ( ) , x ) =x
{}
unc ion In e se(x :G) :G {
−x
}
lemma P oduc In e se(x :G)
ensu es P oduc ( x , I n e s e ( x )) =I d e n i y ( )
ens u s P oduc ( I n e s e ( x ) , x ) =I d e n i y ( )
{}
}
Figu a 2.4: Módulo conc e o que e ina la es uc u a de g upo pa a los en e os.
20 Capí ulo 3. Algo i mos pa a el p ocesamien o de segmen os
in n = l; in = 0; in s = 0;
while (n < . size ()) {
i (!( [n] % 2 == 0)) { s = n + 1; }
i (n + 1 - l >= 0 && s <= n + 1 - l) { ++; }
++n;
}
Figu a 3.4: Algo i mo pa a con a cuán os segmen os de longi ud lcumplen que
odos sus elemen os son pa es
{ = (# p: 0 ≤p−l < p ≤ | |:A( , p −l, q)}
Y, de mane a simila a los an e io es p oblemas, nues o in a ian e es:
{ = (# p: 0 ≤p−l < p ≤n:A( , p −l, q)}
De es a o ma, cuando nues o bucle inalice, hab emos alcanzado la pos condi-
ción.
3.4. O os p oblemas
O os p oblemas que no hemos podido es udia sin:
Exis e un subsegmen o que cumple una p opiedad.
Pa a odo subsegmen o se cumple una p opiedad.
Subsegmen o que cumple una p opiedad al que la suma de sus elemen os es
máxima.
Cabe deci que que los dos p ime os p oblemas son ealmen e uno solo, ya que
comp oba si odos los subsegmen os de un ec o cumplen una p opiedad Aes
equi alen e a comp oba que no exis e ningún segmen o que cumple el con a io de
la p opiedad A. Es os p oblemas se esuel en eco iendo el ec o de un ex emo
a o o, en el p ime caso buscando el segmen o que cumple Ay en el segundo el
segmen o que no cumple A, en ambos casos si encon amos dicho segmen o se de iene
la búsqueda al habe hallado la espues a al p oblema.

Cap´
ı ulo 4
P oblemas de segmen os de longi ud
máxima
En es e capí ulo se p o undiza á en la que ha sido la pa e undamen al del
p oyec o, el es udio de la e i icación de los p oblemas de cálculo del segmen o de
longi ud máxima que cumple una p opiedad dado un ec o de elemen os. Todo el
modelado y e i icación de es os p oblemas en Da ny se encuen a en la ca pe a
seg-long-max del p oyec o.
Du an e el desa ollo del p oyec o se han es udiado di e en es p oblemas y sus
espec i as soluciones. Se han encon ado simili udes y di e encias en e los dis in os
p oblemas, exis iendo pa a algunos casos conc e os algo i mos más e icien es que el
caso gene al pa a su solución, debido p incipalmen e a las ca ac e ís icas y o ma o
de las p opiedades que han de cumpli los segmen os. Es po es o que se hace ne-
cesa io una clasi icación po casos den o de es e ipo de p oblemas, así como una
abs acción común que ag upe las simili udes a la ho a de esol e cada uno de ellos.
De es a o ma un usua io elegi á el módulo más ap opiado pa a esol e su p oblema
y en muchos casos bas a á con que p opo cione los de alles más especí icos de su
p oblema pues o que el módulo ya con iene los elemen os de e i icación necesa ios.
La p ime a sección de es e capí ulo desc ibe es e úl imo p oceso de abs acción,
mien as que la segunda desc ibe la clasi icación que se ha lle ado a cabo du an e
el desa ollo de es e abajo. Finalmen e, en la úl ima sección de es e capí ulo se
mues a un ejemplo que ilus a de mane a conc e a odo lo an e io .
En la Figu a 4.1 se mues a un g á ico de dependencias en e los di e en es mó-
dulos que ep esen an los di e en es ipos de p oblemas, pa a una mejo comp ensión
po pa e del lec o :
A con inuación se o ece una b e e explicación de cada uno de ellos:
SegLongMax es el módulo que abs ae las ca ac e ís icas comunes de odos los
p oblemas de es e ipo, y es del cual odos hab án de he eda .
Abs ac ClosedLe es el módulo que abs ae las ca ac e ís icas comunes de
aquellos p oblemas que, además de se del ipo de es a sección, p esen an una
21
22 Capí ulo 4. P oblemas de segmen os de longi ud máxima
SegLongMax
Abs ac ClosedLe SegLongMaxClosedLe So ed
SegLongMaxFo AllP SegLongMaxRela ion
Figu a 4.1: Diag ama de la elación en a módulos de segmen o de longi ud máxima
p opiedad Aque es ce ada po la izquie da.
SegLongMaxFo AllP es el módulo que abs ae las ca ac e ís icas comunes de aque-
llos p oblemas cuya p opiedad comp ueba si odos los elemen os del segmen o
cumplen una cie a p opiedad.
SegLongMaxRela ion es el módulo que ab ae las ca ac e ís icas comunes de aque-
llos p oblemas cuya p opiedad comp ueba si odo los elemen os del segmen o
cumplen una cie a elación en e cada pa de ellos.
SegLongMaxClosedLe So ed es el módulo que abs ae las ca ac e ís icas comu-
nes de aquellos p oblemas cuya p opiedad es ce ada po la izquie da y iene
como p econdición que los elemen os del ec o es án o denados.
4.1. Modelización del p oblema
Las unciones y mé odos desc i os a con inuación se encuen an en el a chi o
seg_long_max_abs.d y que se enca ga de abs ae aquellos mé odos, unciones y lemas
que son comunes a odos los p oblemas de es e ipo. El iche o con iene un único
módulo abs ac o, SegLongMax, del cual e ina án odos los p oblemas que sean de
es e ipo.
Es os mé odos, unciones y lemas se dejan sin implemen a o e i ica (a excep-
ción de algún caso conc e o), ya que la mane a de implemen a los e icien emen e
a a depende de la p opiedad conc e a que se es é es udiando. En las secciones
siguien es se e ina án pa a ep esen a dis in os g upos de p oblemas.
4.1. Modelización del p oblema 23
me hod mseg_long_max( :a ay<T>) e u ns ( :in )
ensu es he e_is_a_segmen _ ha _long( [..] , )
ensu es is_longes _segmen ( [..] , )
ghos u n c i o n is_longes _segmen (s :seq<T>, :in ):bool
{
∀p:in , q :in | 0 ≤p≤q≤|s|
∧is_ ue_on_segmen (s , p, q) •q−p≤
}
ghos u n c i o n he e_is_a_segmen _ ha _long(s :seq<T>, :in ):bool
{
∃p:in , q :in | 0 ≤p≤q≤|s|
∧is_ ue_on_segmen (s , p, q) •q−p=
}
Figu a 4.2: Especi icación del mé odo m_seg_long_max
Pa a empeza a explo a nues o p oblema, comenzamos especi icando de mane a
o mal el mismo. Pa imos de un ec o de nelemen os y que emos encon a la
longi ud del segmen o que cumple una cie a p opiedad Ade mane a que cualquie
o o segmen o del ec o que cumpla la p opiedad p esen e una longi ud meno o
igual al de uel o:
{n≥0}
me hod seg-long-max( [0...n)) e u n : in
{ = (max p, q : 0 ≤p≤q≤n∧A( , p, q):(q−p)}
El mé odo seglong-max que hemos especi icado es á ep esen ado en nues o mo-
delo po mseg_long_max( : a ay<T>) e u ns ( : in ). Es e mé odo iene como pa-
áme o el ec o que es á siendo es udiado y de uel e el alo que es amos bus-
cando. Es el mé odo p incipal del algo i mo y el que se espe a que el usua io u ilice
a la ho a de modela sus p opios p oblemas.
La pos condición que conc e a las p opiedades que ha de cumpli el alo que
de ol emos es á especi icada en los p edicados is_longes _segmen (s : seq<T>, :
in ) y he e_is_a_segmen _ ha _long(s : seq<T>, : in ) que dados el ec o y el
alo de uel o, asegu an que no exis e ningún segmen o que cumpla la p opiedad
con una longi ud mayo que y que exis e al menos un segmen o que cumple la
p opiedad que iene longi ud , espec i amen e. El mé odo queda especi icado en
la Figu a 4.2.
Obse ación. Nues o mé odo admi e a ay gené icos, pa a una mayo abs acción.
El ipo de los elemen os lo ija á el usua io en el módulo inal cuando de ina la
p opiedad que desea es udia . Es e es ánda se man iene en odos los p oblemas
a ados del abajo.
El que un segmen o cumpla o no la p opiedad iene modelado median e la unción
an asma is_ ue_on_segmen ( : seq<T>, ini : in , in : in ) : bool que dado el
ec o que se es á es udiando y un segmen o [ini, in), de uel e cie o si la p opie-
dad es udiada se cumple pa a los elemen os del segmen o o also en caso con a io.
24 Capí ulo 4. P oblemas de segmen os de longi ud máxima
La p econdición de es a unción es que el pa (ini, in) sean índices álidos del
ec o .
Nues a o ma de abo da el p oblema consis i á en eco e el ec o de izquie -
da a de echa, de mane a que cuando a anzamos lle amos calculado el alo de la
mayo longi ud de los segmen os que cumplen la p opiedad encon ados has a el mo-
men o, es e alo se almacena á en una a iable , que se á el alo que e minemos
de ol iendo al inaliza el bucle.
Además de es a a iable, se u iliza án o as dos: nys, ambos alo es en e os. La
p ime a de ellas (n) ep esen a el índice del ec o an es del cual ya hemos es udiado
odos los posibles segmen os, mien as que la segunda (s) ep esen a el índice del
segmen o más la go al que el segmen o [s, n) cumple la p opiedad. Es e es el
in a ian e que se a a á de man ene en el bucle.
En cada i e ación del bucle inc emen a emos en uno el alo de n, el paso A2del
esquema p esen ado en el Capí ulo 3, y a a emos de man ene el in a ian e con
espec o a las a iables ys, de mane a que al inaliza el mismo hayamos alcanzado
la pos condición.
Pa a pode modela el in a ian e, se ha de inido la unción an asma ghos
unc ion seg_long_max( : seq<T>, ini : in , in : in ) : (in , in ), de inida de ma-
ne a ecu si a. La unción de uel e dos alo es en e os, el p ime o de ellos ep esen a
la longi ud del segmen o más la go que cumple la p opiedad en el segmen o [ini,
in) de . El segundo de ellos ep esen a el índice más pequeño, de mane a que el
segmen o que delimi an es e alo y in cumpla la p opiedad. Es cla o que los alo es
que de uel e es a unción es án muy elacionados con las a iables de p og am y
sque hemos de inido p e iamen e.
Nó ese que si llamamos a la unción con los pa áme os ( , 0, | |), es a nos
de uel e el que es amos buscando. La única p econdición de es a unción es que
(ini, in) sean índices álidos del ec o . De es a o ma la unción queda de inida
de la siguien e o ma:
ghos u n c i o n seg_long_max ( :seq<T>, i n i :in , i n :in ):(i n ,in )
dec eases i n −ini
e q u i e s 0≤ini ≤ i n ≤| |
La azón de exis encia de es a unción es la de sepa a el azonamien o o espe-
ci icación de nues o p oblema de la implemen ación. De es a o ma, odo el azo-
namien o sob e las p opiedades y lemas que amos a hace se basa á en los alo es
de uel os po la unción seg_long_max. Más adelan e en la Sección 4.2 demos a emos
que los alo es de uel os po es a unción cumplen lo exp esado po la especi icación
dada en la Figu a 4.2.
Una ez de inida es a unción, podemos p esen a el in a ian e conc e o que
lle a á nues o mé odo p incipal, que no es más que asegu a que los alo es de y
sque lle amos has a el momen o en nues o eco ido po el ec o se co esponden
con los alo es de la unción se_long_max. Es deci que se cumple que:
4.1. Modelización del p oblema 25
while n < . Leng h
dec eases . Leng h −n
in a ian 0≤s≤n≤ . Leng h
in a ian =seg_long_max ( [ . . ] , 0 , n ) . 0
in a ian s=seg_long_max ( [ . . ] , 0 , n ) . 1
Además de lo an e io , ambién enemos que asegu a nos que los alo es de sy
nsiemp e es án den o de los lími es ma cados po nues o ec o , pa a así pode
sa is ace las p econdiciones de la unción seg_long_max. Como unción de co a se ha
elegido .Leng h - n.
Pa a consegui man ene el in a ian e, se han c eado es mé odos más que an a
se llamados desde el p incipal y que ep esen an los conjun os de ins ucciones A0y
A1. El p ime o de ellos es el mé odo a iable_ini ializa ion( : a ay<T>) e u ns
( : in , s: in , n : in ) que se u iliza pa a inicializa las a iables ya desc i as.
Es e mé odo se co esponde, po an o, con el A0. No p esen a ninguna p econdición
y nos asegu a que los alo es de uel os cumpli án el in a ian e en la en ada en el
bucle. El mé odo queda especi icado así:
me hod a iable_ini ializa ion( :a ay<T>) e u ns ( :in , s :in , n :in )
ensu es 0≤s≤n≤ . Leng h
ensu es =seg_long_max ( [ . . ] , 0 , n ) . 0
ensu es s=seg_long_max ( [ . . ] , 0 , n ) . 1
También se ha especi icado el mé odo upda e_ac ual_s( : a ay<T>, ini : in ,
old_s : in , new_k : in ) e u ns (new_s : in ) que se enca ga de man ene el in-
a ian e espec o la a iable s. Recibe como pa áme os el ec o que es amos es u-
diando, el índice donde se inicia el segmen o que es amos es udiando [ini, new_k)
, el an iguo alo de san es de que ac ualizase el alo de ny el nue o alo de
n, que se supone que ha inc emen ado en uno. Las p econdiciones del mé odo son
que se cumpla el in a ian e pa a los an iguos alo es de syny las pos condiciones
ga an izan que se man iene. El mé odo queda especi icado de la siguien e mane a:
me hod upda e_ac ual_s( :a ay<T>, i n i :in , old_s :in , new_k :in )
e u ns (new_s :in )
e q u i e s 0≤ini ≤old_s < new_k ≤ . Leng h
e q u i e s old_s =seg_long_max ( [ . . ] , i n i , new_k −1 ).1
ensu es 0≤new_s ≤new_k
ensu es new_s =seg_long_max ( [ . . ] , i n i , new_k ) . 1
Finalmen e, se especi ica ambién el mé odo upda e_ac ual_seg_leng h( : a ay<T>,
old_ : in , old_n : in , new_s : in ) e u ns (new_ : in ) que se enca ga de man-
ene el in a ian e con espec o a la a iable . Recibe como pa áme os el ec o que
es amos es udiando , el an iguo alo de , el an iguo alo de ny el nue o alo de
s. Las p econdiciones del mé odo son que se cumplan el in a ian e co espondien e
pa a las a iables del mé odo p incipal ( , s y n), es deci , el de la i e ación an e-
io pa a las a iables que oda ía no han sido ac ualizadas (old_ , old_n) y el de la
ac ual pa a las ac ualizadas (new_s). El mé odo queda en onces especi icado como
sigue:

26 Capí ulo 4. P oblemas de segmen os de longi ud máxima
me hod upda e_ac ual_seg_leng h( :a ay<T>, old_ :i n , old_n :in , new_s :in )
e u ns (new_ :in )
e q u i e s 0≤old_n < . Leng h
e q u i e s old_ =seg_long_max ( [ . . ] , 0 , old_n ) . 0
e q u i e s new_s =seg_long_max ( [ . . ] , 0 , old_n + 1 ) . 1
ensu es new_ =seg_long_max ( [ . . ] , 0 , old_n + 1 ) . 0
Es os dos úl imos mé odos se co esponden con el conjun o de ins ucciones A1
del Capí ulo 3.
4.2. Demos ación de la co ección
Una ez especi icados odos es os mé odos y unciones, debemos implemen a
aquellos que sean gene ales pa a odos los ipos de p oblemas y, lo más impo an e
de odo, debemos se capaces de consegui que Da ny e i ique nues o código.
A con inuación amos a p esen a una se ie de lemas que son comunes a odos
los ipos de p oblemas que hemos es udiado y que nos an a pe mi i guia a Da ny
en la e i icación de es os mé odos.
Los más impo an es son los lemas: seg_long_max_exis ence( : seq<T>, ini :
in , in : in ) yseg_long_max_snd( : seq<T>, ini : in , in : in ). Es os lemas
se c ean pa a pe mi i a Da ny deduci las pos condiciones a pa i del in a ian e y
la negación de la condición de salida de nues o bucle, es deci , una ez e minada
la ejecución del bucle.
Ambos lemas eciben el ec o es udiado y los índices de inicio y in del seg-
men o que se es á es udiando (ini, in). La única p econdición que p esen an es
que ambos índices es én den o de los alo es pe mi idos po nues o sean álidos.
El p ime o de ellos, seg_long_max_exis ence nos asegu a que exis en segmen os
den o de los lími es de inidos en nues o ec o que cumplen la p opiedad es udiada,
ales que al menos uno enga la longi ud del p ime alo de uel o po seg-long-max
y al que al menos exis a uno que e mine incluyendo el úl imo índice del ec-
o , y además enga como p ime índice el segundo alo de uel o po la unción
seg-long-max.
El segundo de ellos, seg_long_max_snd nos asegu a que el p ime alo de uel o
po la unción seg-long-max es mayo o igual que la longi ud de cualquie segmen o
que cumpla la p opiedad den o de los lími es de inidos po los índices pasados como
pa áme os. P esen amos los lemas a con inuación:
lemma seg_long_max_exis ence( :seq<T>, i n i :in , i n :in )
e q u i e s 0≤ini ≤ i n ≤| |
ensu es ∃p , q | i n i ≤p≤q≤ i n ∧is_ ue_on_segmen ( , p, q)
•q−p=seg_long_max ( , i n i , i n ) . 0
ensu es ∃p | i n i ≤p≤ i n ∧is_ ue_on_segmen ( , p , i n )
•p=seg_long_max ( , i n i , i n ) . 1
lemma seg_long_max_snd ( :seq<T>, i n i :i n , i n :in )
e q u i e s 0≤ini ≤ i n ≤| |
ensu es ∀p , q | i n i ≤p≤q≤ i n ∧is_ ue_on_segmen ( , p, q)
•q−p≤seg_long_max ( , i n i , i n ) . 0
4.3. Abs acción y conc eción sob e los p oblemas 27
Es os son los dos lemas que se u ilizan pa a p oba las pos condiciones den o
del mé odo p incipal, pe o en es e módulo ambién se han incluido o os lemas
que mues an p opiedades undamen ales y ú iles de la unción seg-long-max y que
se ha decidido inclui en el mismo, pues se u ilizan mucho en cualquie a de los
ipos de p oblemas es udiados. Además, los es lemas nos ayudan y guían a la
ho a de azona sob e cómo implemen a la unción seg-long-max, ya que limi an
sensiblemen e los posibles alo es que es a puede de ol e y nos o ien a sob e su
inalidad den o del modelo.
El p ime o de ellos es el lema allways_g (s : seq<T>, in : in ) que nos asegu a
que el p ime alo de uel o po la unción seg-long-max in ocada con los pa áme os
(s, 0, in) es siemp e mayo que la di e encia en e in y el segundo alo de uel o
po seg-long-max. La única p econdición del mé odo es que el pa áme o in sea un
índice álido del ec o s. Es o es así po que el p ime alo del pa con empla odos
lo subsegmen os del ec o , mien as que el segundo alo del pa solo con empla
aquellos cuyo ex emo supe io es in.
lemma allways_g (s :seq<T>, i n :in )
e q u i e s 0≤ i n ≤|s|
ensu es seg_long_max ( s , 0 , i n ) . 0 ≥ i n −seg_long_max ( s , 0 , i n ) . 1
Los dos lemas es an es nos p opo cionan in o mación sob e los lími es de los
alo es de uel os po la unción seg-long-max; son seg_long_max_g (s : seq<T>, ini
: in , in : in ) yuppe _limi (s : seq<T>, ini : in , in : in ). La p econdición
de ambos mé odos es que los índices (ini, in) con los que se in oca la unción
seg-long-max sean índices álidos con espec o al ec o s. Es a p econdición es com-
pa ida po muchos lemas, po lo que a pa i de aho a solo apa ece á en el códi-
go de los lemas. El p ime o de ellos nos asegu a que el p ime alo de uel o po
seg-long-max es mayo o igual que 0. El segundo nos asegu a que el segundo alo
de uel o po la unción seg-long-max es meno o igual que el índice in.
lemma seg_long_max_g ( s :seq<T>, i n i :in , i n :in )
e q u i e s 0≤ini ≤ i n ≤|s| // Es aba e s i c o an es
ensu es seg_long_max ( s , i n i , i n ) . 0 ≥0
lemma uppe _limi (s :seq<T>, i n i :i n , i n :in )
dec eases i n −ini
e q u i e s 0≤i n i < i n ≤|s|
ensu es seg_long_max ( s , i n i , i n ) . 1 ≤ i n
Una ez p esen ado el modelo gene al que segui án odos los p oblemas de es e
ipo, podemos pasa a lle a una clasi icación más exhaus i a en unción de las
ca ac e ís icas de las p opiedades A.
4.3. Abs acción y conc eción sob e los p oblemas
En la p ime a sección se ha lle ado a cabo una desc ipción de los mé odos, le-
mas y unciones que se han u ilizado en las soluciones p esen adas pa a algo i mos
28 Capí ulo 4. P oblemas de segmen os de longi ud máxima
de segmen o de longi ud máxima. En es a amos a dis ingui di e en es conjun os
de p oblemas que compa en una se ie de ca ac e ís icas comunes que nos pe mi-
en esol e los de mane a simila . Cada uno de es os sub ipos de p oblemas e ina
el módulo abs ac o p esen ado en la an e io sección y iene acompañado de un
ejemplo conc e o en el eposi o io del abajo.
4.3.1. P opiedades ce adas po la izquie da
Nues o abajo se ha cen ado en es udia p oblemas cuyas p opiedades p esen-
asen la ca ac e ís ica de se ce adas po la izquie da, aunque ambién se mues a
en el a chi o es _abs ac .d y cómo implemen a con nues o modelo un p oblema
que no p esen e es e ipo de p opiedades.
Es e ipo de p oblemas son más in e esan es, pues o ecen la posibilidad de lle a
a cabo algo i mos que los solucionen de mane a más e icien e, con cos e en la mayo
pa e de los casos lineales, al con a io que si no p esen asen es a p opiedad, ya
que en el caso gene al los algo i mos se án al menos de cos e cuad á ico, ya que
debe emos es udia odos los posibles segmen os al a anza en uno el índice de
nues a a iable n.
Es po es o que, con el obje i o de p esen a con mayo cla idad las p opiedades
que dis inguen es os p oblemas y las elaciones en e los di e en es ipos de p oble-
mas, se ha de inido el módulo Abs ac ClosedLe , que e ina el módulo SegLongMax.
En es e módulo es án basados odos los ipos de p oblemas que se p esen a án a
con inuación.
El elemen o más impo an e que con iene el módulo es el lema closed_on_le -
_lemma, el cual, si se demues a pa a la p opiedad Aes udiada, implica que Ap esen a
la ca ac e ís ica de se ce ada po la izquie da. Se p esen a a con inuación:
lemma closed_on_le _lemma()
ensu es ∀i n i , i n , p , s :seq<T> | 0 ≤ini ≤p≤ i n ≤|s|
∧is_ ue_on_segmen ( s , i n i , i n ) •is_ ue_on_segmen ( s , i n i , p )
Del lema an e io se puede deduci , aunque hay que adap a lo a cada ipo de
p oblema, el lema no_need_ o_come_back(s : seq<T>, ini : in , in : in ) que nos
asegu a que pa a cualquie índice in e io al alo del segundo alo de uel o po la
unción seg-long-max, el segmen o [p, in)no puede cumpli la p opiedad. El lema
queda de inido de la siguien e mane a:
lemma no_need_ o_come_back ( s :seq<T>, i n i :in , i n :in )
e q u i e s 0≤i n i < i n ≤|s|
ensu es ∀p:in | i n i ≤p < seg_long_max ( s , i n i , i n ) . 1 ≤ i n
• ¬is_ ue_on_segmen ( s , p , i n )
Es os lemas se dejan sin demos a , pa a que sea el usua io el que, con base en
la p opiedad es udiada, demues e que se cumplen. Es os lemas se demues an de
mane a muy simila , ya que bas a con lle a a cabo una demos ación po educción
al absu do u ilizando el lema closed_on_le _lemma.
4.3. Abs acción y conc eción sob e los p oblemas 29
Además de los lemas an e io es, p esen amos una implemen ación común del
mé odo p incipal que an a compa i odos los p oblemas que p esen en la ca-
ac e ís ica de se ce ados po la izquie da. Todos los mé odos, unciones, lemas,
in a ian es y a iables u ilizados ya han sido p esen ados, po lo que nos limi a emos
a mos a el código del cue po del mé odo p incipal:
a n , s ;
, s , n := a iable_ini ializa ion( );
while n < . Leng h
dec eases . Leng h −n
in a ian 0≤s≤n≤ . Leng h
in a ian =seg_long_max ( [ . . ] , 0 , n ) . 0
in a ian s=seg_long_max ( [ . . ] , 0 , n ) . 1
{
s:= upda e_ac ual_s ( , 0 , s , n + 1 ) ;
:= upda e_ac ual_seg_leng h( , , n, s );
n:= n + 1 ;
}
seg_long_max_exis ence ( [ . . ] , 0 , . Leng h ) ;
seg_long_max_snd ( [ . . ] , 0 , . Leng h ) ;
Como se puede obse a , el mé odo sigue el esquema p esen ado en el Capí ulo
3, y podemos deduci las pos condiciones a pa i de los lemas p esen ados. G acias
a es os lemas y a los in a ian es p esen ados, nues o mé odo es acep ado po Da ny,
que nos con i ma su co ección.
4.3.2. P opiedades uni e sales sob e elemen os
El código en Da ny de es a subsección lo podemos encon a en el módulo Seg-
LongMaxUni a y que e ina a Abs ac ClosedLe . Es e módulo se encuen a en el a -
chi o /seg-long-max/gene al/uni a y/uni a y.d y del p oyec o.
Es e ipo de p oblemas se basan en una p opiedad Asob e el segmen o que
comp ueba si pa a cada elemen o del segmen o en cues ión se cumple una cie a
p opiedad P. De es a o ma, podemos modela la ya de inida unción an asma
is_ ue_on_segmen de la siguien e mane a:
ghos u n c i o n is_ ue_on_segmen ( :seq<T>, i n i :in , i n :in ):bool
{
∀p | i n i ≤p < i n •is_ ue_on_elem( [p])
}
Debido a es e o ma o de la p opiedad A, sabemos que es a iene dos cualidades que
se án muy impo an es a la ho a de elegi nues a solución: es cie a pa a segmen os
acíos y es ce ada po la izquie da. La unción is_ ue_on_elem(elem : T) se deja
sin implemen a pa a que sea el usua io el que implemen e la p opiedad que quie a
comp oba :
36 Capí ulo 4. P oblemas de segmen os de longi ud máxima
La azón po la que no se e ina es e módulo explíci amen e es po que Da ny no
pe mi e modi ica las p econdiciones de mé odos/ unciones/lemas que es én de ini-
das en un módulo supe io , po lo que al eque i una p econdición adicional, en es e
caso que el ec o es é o denado, se ha decidido segui la misma es uc u a que en
el es o de módulos pe o sin hace explíci a es a elación. Es e módulo se encuen a
en el a chi o /seg_long_max/closed_le _so ed/closed_le _so ed.d y del p oyec o.
Las p incipales ca ac e ís icas de es e módulo son, po un lado, la de inición e
inclusión como p econdición que el ec o es udiado es é o denado y, po o o,
el al o g ado de gene alización, ya que las p opiedades que es amos es udiando son
aquellas que son p opiedades sob e segmen os a las que solo les pedimos que sean
ce adas po la izquie da y cie as pa a el segmen o acío.
En ealidad, nues o módulo se i ía pa a modela cualquie p opiedad que sea
ce ada po la izquie da y cie a pa a segmen os acíos, sin necesidad de exigi que
el ec o es é o denado. La azón po la que se incluye es a p econdición es po que
en el ejemplo que se ha elegido pa a ep esen a es e ipo de p oblemas es necesa io
que el ec o es é o denado pa a que la p opiedad que se es udia sea ce ada po la
izquie da, po lo que debemos inclui lo en el módulo abs ac o como p econdición,
pues sino Da ny no nos deja ía modi ica la p econdición en el módulo conc e o.
Pa a modela la p opiedad que a a de e mina el p oblema a esol e , nos a-
lemos de la ya de inida is_ ue_on_segmen que dejamos sin implemen a pa a que
sea el usua io el que la implemen e en unción de la p opiedad que es á es udian-
do. De mane a pa alela de inimos el mé odo m_ ue_on_segmen ( : a ay<T>, ini :
in , in : in ) e u ns ( es : bool) que nos a a se i pa a man ene la sepa a-
ción en e especi icación e implemen ación, es e mé odo ambién se deja pa a que lo
implemen e el usua io. El nue o mé odo queda de inido de la siguien e mane a:
me hod m_ ue_on_segmen ( :a ay<T>, i n i :i n , i n :in ) e u ns ( e s :bool )
e q u i e s 0≤ini ≤ i n ≤ . Leng h
ensu es e s =is_ ue_on_segmen ( [ . . ] , i n i , i n )
Como es e módulo engloba a odas aquellas p opiedades que son ce adas po
la izquie da y cie as pa a segmen os acíos, en pa icula es posible modela los
p oblemas ya desc i os en los apa ados an e io es.
La azón pa a a a los como casos apa e es que en esos p oblemas es posible
consegui una solución más e icien e, ya que podemos, cuando aumen amos en uno
el alo de la a iable n, simplemen e comp oba si se cumple una cie a p opiedad
PoRen los úl imos elemen os del ec o y en caso de que no se cumpla, de ol e
el segmen o más pequeño pa a el que la p opiedad siemp e es cie a (el acío o el
de un solo elemen o). Aho a, en cambio, necesi a emos i comp obando pa a cada
índice pen e el an iguo alo de sy in si se cumple la p opiedad pa a el segmen o
[p, in)
Es o es lo que mo i a la de inición de una nue a unción an asma ecu si a
que a a modela es e compo amien o de nues o algo i mo, y es la que usa emos
después en la especi icación pa a de ini un in a ian e que nos pe mi e alcanza la
pos condición de los mé odos que ya hemos de inido. También la usa emos pa a

4.3. Abs acción y conc eción sob e los p oblemas 37
de ini y demos a di e en es lemas que ayuda án a Da ny a lle a a cabo la e i-
icación. Es a nue a unción es upda e_s( : seq<T>, ini : in , in : in ) : (in ).
La unción ecibe los mismos pa áme os que su unción he mana seg_long_max, y
p esen a la misma p econdición. La unción se llama desde es a unción, y se u iliza
pa a calcula el segundo alo (es deci , la a iable s) en el caso en que no se cumple
la p opiedad pa a el segmen o [ini, in). La unción dis ingue es casos:
1. Si ini == in en onces hemos llegado al caso acío y, como la p opiedad es
cie a pa a segmen os acíos, en pa icula es cie a pa a el segmen o [ini,
ini) po lo que de ol emos ini.
2. Si la p opiedad es cie a en el segmen o ac ual, en onces ambién de ol emos
el alo ini.
3. En caso con a io, seguimos buscando un sadecuado, po lo que hacemos una
llamada ecu si a aumen ando en 1el alo de ini.
Cabe deci que Da ny no es capaz de de ini una unción de co a adecuada, po lo
que se le ha p opo cionado una explíci a ( in - ini). Es a unción de co a ambién
se á necesa ia inclui la pa a los lemas que azonen sob e las p opiedades de es a
unción. La unción, po an o, queda implemen ada de la siguien e mane a:
ghos u n c i o n upda e_s( :seq<T>, i n i :i n , i n :in ):(in )
dec eases i n −ini
e q u i e s 0≤ini ≤ i n ≤| |
{
i ( i n i = i n ) hen ini
e l s e i ( is_ ue_on_segmen ( , i n i , i n ) ) hen ini
else upda e_s ( , i n i + 1 , i n )
}
Pa a de ini la p opiedad de que un ec o es é o denado, hemos enido que
de ini el p edicado so ed y ambién ija un ipo en es e módulo abs ac o, ya que
en Da ny no exis e un conjun o que englobe a odos los ipos compa ables. Po lo
an o:
ype T = in
ghos p e d i c a e s o e d ( s :seq<T>)
{
∀p:in , q :in | 0 ≤p≤q < | s | •s [ p ] ≤s [ q ]
}
Pa a ayuda nos en la e i icación, se han incluido una se ie de lemas adicionales
que p esen amos en la Figu a 4.4. La mayo ía nos apo an in o mación sob e las
p opiedades que cumple la nue a unción que hemos de inido, aunque hay algún
lema nue o sob e la unción seg_long_max, pe o es e lo explica emos al inal de la
sección con el es o de lemas an e io es.
El p ime lema que p esen amos es upda e_s_limi s( : seq<T>, ini : in , in
: in ) el cual nos pe mi e asegu a que el alo de la unción es a á aco ado po
es os mismos índices.
38 Capí ulo 4. P oblemas de segmen os de longi ud máxima
lemma upda e_s_limi s( :seq<T>, i n i :in , i n :in )
dec eases i n −ini
e q u i e s 0≤ini ≤ i n ≤| |
ensu es ini ≤upda e_s ( , i n i , i n ) ≤ i n
lemma upda e_s_good_segmen ( :seq<T>, i n i :i n , i n :in )
dec eases i n −ini
e q u i e s 0≤ini ≤ i n ≤| |
e q u i e s ini ≤upda e_s ( , i n i , i n ) ≤ i n
ensu es is_ ue_on_segmen ( , upda e_s ( , i ni , i n ) , i n )
lemma upda e_s_is_seg_long_1( :seq<T>, i n i :i n , i n :in )
dec eases i n −ini
e q u i e s 0≤ini ≤ i n ≤| |
e q u i e s s o e d ( )
ensu es seg_long_max ( , i n i , i n ) . 1 =upda e_s ( , i n i , i n )
lemma upda e_s_min_ alue( :seq<T>, i n i :i n , i n :in )
dec eases i n −ini
e q u i e s 0≤ini ≤ i n ≤| |
ensu es ∀p | i n i ≤p≤ i n
∧is_ ue_on_segmen ( , p , i n ) •upda e_s ( , i n i , i n ) ≤p
lemma upda e_s_i _snd( :seq<T>, i n i :i n , old_s :i n , i n :in )
e q u i e s 0≤i n i < i n ≤| |
e q u i e s s o e d ( )
e q u i e s ini ≤old_s ≤ i n
e q u i e s old_s =upda e_s ( , i n i , i n −1)
ensu es upda e_s ( , i n i , i n ) =upda e_s ( , old_s , i n )
Figu a 4.4: P opiedades de upda e_s pa a el caso ce ado po la izquie da con ec o
o denado.
El siguien e lema que p esen amos es upda e_s_good_segmen ( : seq<T>, ini :
in , in : in ) el cual nos exige que el alo de uel o po la unción upda e_s se
encuen e aco ado po (ini, in), y nos asegu a que el alo de uel o po la unción
o ma, jun o al índice in, un segmen o que cumple la p opiedad.
El lema upda e_s_is_seg_long_1( : seq<T>, ini : in , in : in ) nos asegu a
que el segundo alo de uel o po la unción seg_long_max es el mismo que el de-
uel o po la unción upda e_s.
El siguien e lema es upda e_s_min_ alue( : seq<T>, ini : in , in : in ) el cual
es muy simila al ya de inido no_need_ o_come_back. Dados un pa de índices adecua-
dos pa a nues o ec o , nos asegu a que pa a cualquie píndice del ec o al que
la p opiedad sea cie a en el segmen o [p, in) en onces sabemos que pes mayo
o igual que el alo de uel o po la unción upda e_s cuando es in ocada con los
pa áme os que le pasamos al lema en cues ión.
Finalmen e, p esen amos el lema upda e_s_i _snd( : seq<T>, ini : in , old_s
: in , in : in ) que nos asegu a que si llamamos a la unción upda e_s con los
pa áme os ( , ini, in) y( , old_s, in) en onces nos de uel e el mismo índice.
Además de es os lemas sob e la unción upda e_s, se ha de inido un nue o le-
ma sob e la unción seg_long_max,seg_long_max_1_is_ini( : seq<T>, ini : in , in
: in ). Es e lema nos exige que le p opo cionemos índices (ini, in) álidos con
4.3. Abs acción y conc eción sob e los p oblemas 39
espec o al ec o , que el ec o es é o denado y que además el segmen o de inido
po [ini, in) cumpla la p opiedad es udiada. Si es o es cie o, en onces el lema nos
asegu a que el segundo alo de uel o po la unción seg_long_max es el p opio ini.
Queda así de inido:
lemma seg_long_max_1_is_ini( :seq<T>, i n i :in , i n :in )
e q u i e s 0≤ini ≤ i n ≤| |
e q u i e s s o e d ( )
e q u i e s is_ ue_on_segmen ( , i n i , i n )
ensu es seg_long_max ( , i n i , i n ) . 1 =ini
Una ez que se han is o las nue as unciones y lemas, eamos cómo se han imple-
men ado las ya conocidas unciones y mé odos. Empecemos po la unción ecu si a
seg_long_max. La unción es á de inida de mane a simila a los casos an e io es, de
nue o dis inguimos es casos:
1. Si ini == in en onces nos encon amos en el caso base y como nues a p o-
piedad es cie a pa a segmen os acíos de ol e mos el pa (0, ini).
2. Si nues o segmen o no cumple la p opiedad en onces de ol emos como p ime
alo el máximo en e el segmen o más la go has a aho a y la longi ud del
nue o segmen o que cumple la p opiedad new_s, in y como segundo alo ,
como debemos ac ualiza s, llamamos a la unción upda e_s( , ini, in).
3. Si nues o segmen o cumple la p opiedad, de nue o como p ime alo de ol e-
mos el máximo que hemos desc i o en el caso en que el segmen o no cumpliese
la p opiedad y como segundo alo de ol emos el sque lle ásemos has a aho a.
La unción queda po an o implemen ada de la siguien e mane a:
ghos u n c i o n seg_long_max ( :seq<T>, i n i :in , i n :in ):(i n ,in )
e q u i e s 0≤ini ≤ i n ≤| |
{
i ( i n i = i n ) hen (0 , i n i )
e l s e i (¬is_ ue_on_segmen ( , i n i , i n ) ) hen
(max( seg_long_max ( , i n i , i n −1 ) . 0 , i n −upda e_s ( , i n i , i n ) ) ,
upda e_s ( , i n i , i n ) )
else
(max( seg_long_max ( , i n i , i n −1 ) . 0 ,
i n −seg_long_max ( , i n i , i n −1 ) . 1 ) ,
seg_long_max ( , i n i , i n −1).1)
}
Veamos aho a cómo se implemen an los mé odos una ez que ya se han im-
plemen ado odas las unciones que an modela su compo amien o. En el caso
de a iable_ini ializa ion, como de nue o la p opiedad es cie a pa a segmen os
acíos se implemen a exac amen e igual que en los casos an e io es. También el mé-
odo upda e_ac ual_seg_leng h es muy simila a los an e io es. Es po eso que no los
mos amos.
Es el mé odo upda e_ac ual_s el que cambia más con espec o a sus an eceso-
es, ya que aho a no a a se su icien e con comp oba una p opiedad y ac ualiza
40 Capí ulo 4. P oblemas de segmen os de longi ud máxima
siemp e al mismo índice, sino que amos a ene que lle a a cabo un bucle en el
que amos p obando uno a uno los posibles candida os. Es en es e mé odo donde se
u ilizan odos los lemas de inidos en es e módulo, ya que debemos asegu a nos que
las a iables cumplen el in a ian e del bucle en la en ada, lo man ienen du an e las
i e aciones y, cuando el bucle e mina, somos capaces de ob ene la pos condición
del mé odo.
Comenzamos asignando a una nue a a iable new_s el alo del an iguo s, y en
cada uel a del bucle comp obamos si pa a el nue e segmen o [new_s, new_n) se
cumple la p opiedad, si no se cumple aumen amos en 1el alo de la a iable. El
in a ian e que man enemos en el bucle iene dos pa es, la p ime a que la a iable
new_s siemp e sea meno o igual que upda e_s( , old_s, new_n) y que la a iable
booleana cond que nos si e pa a comp oba la condición del bucle se man iene
ac ualizada. El mé odo queda implemen ado de la siguien e mane a:
me hod upda e_ac ual_s( :a ay<T>, i n i :in , old_s :i n , new_k :in )
e u ns (new_s :in )
e q u i e s 0≤ini ≤old_s < new_k ≤ . Leng h
e q u i e s s o e d ( [ . . ] )
e q u i e s old_s =seg_long_max ( [ . . ] , i n i , new_k −1 ).1
ensu es 0≤new_s ≤new_k
ensu es new_s =seg_long_max ( [ . . ] , i n i , new_k ) . 1
{
new_s := old_s ;
upda e_s_limi s ( [ . . ] , old_s , new_k ) ;
a cond := m_ ue_on_segmen ( , new_s , new_k ) ;
while(¬cond)
dec eases new_k −new_s
in a ian new_s ≤upda e_s ( [ . . ] , old_s , new_k)
in a ian cond =is_ ue_on_segmen ( [ . . ] , new_s , new_k)
{
upda e_s_good_segmen ( [ . . ] , old_s , new_k ) ;
new_s := new_s + 1 ;
cond := m_ ue_on_segmen ( , new_s , new_k ) ;
}
upda e_s_min_ alue ( [ . . ] , i n i , new_k ) ;
upda e_s_is_seg_long_1 ( [ . . ] , i n i , new_k −1);
a s s e is_ ue_on_segmen ( [ . . ] , new_s , new_k ) ;
upda e_s_i _snd ( [ . . ] , i n i , old_s , new_k ) ;
}
El mé odo p incipal es exac amen e el mismo que el que se p esen ó en la sub-
sección sob e p opiedades ce adas po la izquie da, po lo que no se mues a. Se
deja al usua io que demues e pa a la p opiedad que es á es udiando los lemas si-
guien es, que se u ilizan en la demos ación del es o de lemas de inidos en secciones
an e io es.
En p ime luga , se de ine de nue o el lema closed_on_le _lemma(s : seq<T>) de
una mane a lige amen e di e en e a como lo habíamos p esen ado an es. Aho a el
ec o es udiado lo pasamos como pa áme o y además se le a a pedi al ec o que
es é o denado. El p edicado que ha de cumpli es el mismo que en casos an e io es.
Así pues:
4.3. Abs acción y conc eción sob e los p oblemas 41
lemma closed_on_le _lemma(s :seq<T>)
e q u i e s s o e d ( s )
ensu es ∀i n i , i n , p | 0 ≤ini ≤p≤ i n ≤|s|
∧is_ ue_on_segmen ( s , i n i , i n ) •is_ ue_on_segmen ( s , i n i , p )
En segundo luga , se de ine un lema pa a exp esa que la p opiedad es cie a pa a
el segmen o acío, que en nues o caso iene ep esen ado po los segmen os cuyo
inicio y in son el mismo. De es a o ma, el lema p op_is_ ue_on_ oid( : seq<T>)
queda de inido de la siguien e mane a:
lemma p op_is_ ue_on_ oid( :seq<T>)
ensu es ∀p | 0 ≤p≤| | •is_ ue_on_segmen ( , p, p)
4.3.5. Ejemplo
El ejemplo elegido se ha ex aído de los Apun es de la asigna u a de Es uc-
u as de da os y algo i mos [12], y el algo i mo de esolución es el mismo pa a el
p oblema de Acep a el e o sob e El homb e de seis dedos [10]. La implemen a-
ción del código que se mues a a con inuación la podemos encon a en el módu-
lo Tes ClosedLe So ed en el a chi o /seg_long_max/closed_le _so ed/ es .d y. El
p oblema que amos a es udia es el siguien e:
P oblema. Dada un ec o de en e os o denado, que emos sabe la longi ud del
segmen o más la go que cumple que la di e encia en e odos sus elemen os es meno
que una cie a can idad ija.
La especi icación del mé odo que que emos ob ene es la siguien e:
{1≤n∧k≥1∧so ed( )}
me hod seg-long-max( [0...n)) e u n : in
{ = (max p, q : 0 ≤p≤q≤leng h( )∧( [q]− [p]< k):(q−p)}
Los ex ac os de código que se an a mos a a con inuación pueden encon a se
en el iche o /seg_long_max/closed_le _so ed/ es .d y del p oyec o.
Lo p ime o que debemos ija nos es que es e p oblema es uno de los ipos que
hemos p esen ado, es un p oblema cuya p opiedad es ce ada po la izquie da y que
que es cie a pa a segmen os acíos. Sabiendo es o, debemos c ea un mue o módulo
no abs ac o que a a e ina a nues o módulo SegLongMaxClosedLe So ed.
Lo p ime o que debemos hace es ija el pa áme o k. Una ez hecho hecho es o,
debemos de ini la unción is_ ue_on_segmen y el mé odo m_ ue_on_segmen , aco de
a nues a p opiedad. Es o apa ece e lejado en el Figu a 4.5
Aho a debemos demos a los lemas closed_on_le _lemma yp op_is_ ue_on_ oid
que hemos de inido en el módulo abs ac o. En es e caso Da ny es capaz de e i ica lo
sin ayuda. Es e p oceso apa ece e lejado en la Figu a 4.6
Finalmen e, c eamos un mé odo que llama á a nues o mé odo p incipal y u ili-
za á nues as pos condiciones pa a demos a unas pos condiciones equi alen es que

42 Capí ulo 4. P oblemas de segmen os de longi ud máxima
cons k :in := 4
ghos u n c i o n is_ ue_on_segmen ( :seq<T>, i n i :in , i n :in ):(bool )
{
i ( i n i = i n ) hen u e e l s e [ i n −1] − [ i n i ] < k
}
me hod m_ ue_on_segmen ( :a ay<T>, i n i :i n , i n :in )
e u ns ( e s :bool )
{
e s := ue ;
i ( i n i = i n ) { e s := [ i n −1] − [ i n i ] < k ; }
}
Figu a 4.5: Especi iación e implemen ación de la di e encia aco ada
lemma closed_on_le _lemma(s :seq<T>)
{}
lemma p op_is_ ue_on_ oid( :seq<T>)
ensu es ∀p | 0 ≤p≤| | •is_ ue_on_segmen ( , p, p)
{}
Figu a 4.6: Lemas pa a el p oblema de las di e encias aco adas
hacen explíci a las p opiedades que cumple nues o . Es e mé odo es el que apa ece
en la Figu a 4.7.
4.3. Abs acción y conc eción sob e los p oblemas 43
me hod mseg_long_max_ze o ( a :a ay<in >) e u ns ( :in )
e q u i e s s o e d ( a [ . . ] )
e q u i e s ∃p , q | 0 ≤p≤q≤| a [ . . ] |
∧( a [ q −1 ] −a [ p ] < k ) •q−p > 1
ensu es ∀p , q | 0 ≤p≤q≤| a [ . . ] |
∧( a [ q −1 ] −a [ p ] < k ) •q−p≤
ensu es ∃p , q | 0 ≤p≤q≤| a [ . . ] |
∧( a [ q −1 ] −a [ p ] < k ) •q−p=
{
:= mseg_long_max(a );
}
Figu a 4.7: Mé odo p incipal de las di e encias aco adas
Cap´
ı ulo 5
P oblemas de con a segmen os
En es e capí ulo se p o undiza á en el es udio de la e i icación de los p oblemas
de con eo de segmen os que cumplen una cie a p opiedad. Los a chi os que se co es-
ponden con es e capí ulo se encuen an en las ca pe as /con _seg y/sliding_window.
A la ho a de a on a la e i icación de es e ipo de p oblemas, se han a ado de
mane a muy simila a los de segmen o de longi ud máxima, aunque en es e caso no
se ha podido p o undiza an o, po lo que no se ha podido ealiza una clasi icación
de los p oblemas an exhaus i a.
La es uc u a de es e capí ulo es, po an o, muy simila a la del an e io . Se
comienza explicando la abs acción ealizada sob e es e ipo de p oblemas, se p e-
sen a un ipo de p oblemas pa a los que podemos ob ene una solución más e icien e
y se ilus a con un ejemplo conc e o. También se dedica á una sección al ipo de
p oblemas llamados de “ en ana deslizan e”, que son un sub ipo de es os p oblemas.
5.1. Modelado del p oblema
El modelado del p oblema se encuen a con enido en el módulo Con Seg, que a
su ez se encuen a en el iche o /con _seg/con _seg.d y. Es e módulo es el que a la
ho a de ins ancia p oblemas conc e os el usua io debe á e ina , y adap a lo a la
p opiedad conc e a es udiada.
Comenzamos especi icando el ipo de p oblemas que amos a es udia . Pa imos
de un ec o de nelemen os y que emos de ol e un en e o igual al núme o
de segmen os no acíos del ec o ales que cumplen una cie a p opiedad sob e
segmen os A. Podemos esc ibi :
P econdición :{n≥0}
me hod con -seg( [0...n)) e u n : in
Pos condición :{ = (# p, q : 0 ≤p<q≤n:A( , p, q)}
Pa a modela la p opiedad A, se ha u ilizado la misma unción is_ ue_on_segmen
que en el capí ulo an e io .
45
52 Capí ulo 5. P oblemas de con a segmen os
lemma alid_segmen s_ ixed_las _coun ( :seq<T>, i n i :i n , i n :in )
dec eases i n −ini
e q u i e s 0≤ini ≤ i n ≤| |
ensu es ( i n −min_pos_ al ( , i n i , i n ) ) =| alid_segmen s_ ixed_las ( , ini , in )|
Figu a 5.2: Lema alid_segmen s_ ixed_las _coun de con a segmen os.
lemma alid_segmen s_second( :seq<T>, i n i :i n , i n :in )
e q u i e s 0≤ini ≤ i n < | |
ensu es ∀p , q | ( p , q ) i n alid_segm en s ( , i n i , i n ) •q≤ i n
El úl imo lema que de inimos es alid_segmen s_ oid_in e sec ion( : seq<T>,
in : in ) que nos asegu a que la in e sección en e los conjun os que se mues an
es acía. Es a p opiedad es necesa ia pa a azona sob e el ca dinal de la unión,
ya que el ca dinal se ac ualiza sumando la can idad de segmen os que cumplen
la p opiedad que no con emplábamos en el caso en que el ex emo de echo e a
in. Podemos p ocede de es a o ma po que los nue os segmen os, al con ene al
elemen o [ in], no p esen an elemen os comunes con los ya calculados.
lemma alid_segmen s_ oid_in e sec ion( :seq<T>, i n :in )
e q u i e s 0≤ i n < | |
ensu es alid_segmen s ( , 0 , i n ) ∗ alid_segmen s_ ixed_las ( , 0, in + 1) ={}
Finalmen e, queda po deci que odos los lemas que se han de inido en es e
módulo, y aquellos que quedaban po demos a en el módulo supe io , han sido
e i icado po Da ny, con las indicaciones pe inen es pa a ello.
5.3. Ejemplo
El ejemplo que se p esen a a con inuación es á implemen ado en el módulo
Tes Con Seg del a chi o /con _seg/ es .d y de nues o p oyec o.
Pa a e mina de habla de es e ipo de p oblemas de con a segmen os, amos
a e cómo se pod ía u iliza el modelo de inido pa a abaja con una p opiedad
conc e a. El p oblema que hemos elegido es el siguien e:
{n≥0}
me hod con -seg( [0...N)) e u n : in
{ = (# p, q : 0 ≤p<q≤n∧(∀k:p≤k < q : [k] == 0}
Es deci , es amos es udiando el núme o de segmen os den o del ec o ales que
odos sus elemen os son 0. Pa a modela es e p oblema espec o a nues o modelo, lo
p ime o que debemos hace c ea un nue o módulo que implemen e nues o ejemplo
y que e ine alguno de los módulos abs ac os que hemos de inido en la sección
an e io .

5.4. P oblemas de en ana deslizan e 53
Como nues a p opiedad es del ipo es udiado en la úl ima sección, e inamos el
módulo Con SegFo AllP. Como amos a abaja con ec o es de en e os, ijamos el i-
po abs ac o Tal ipo de los en e os. Lo siguien e que debemos hace es implemen a
la unción que modela el p edicado Py el mé odo co espondien e:
ype T = in
ghos u n c i o n is_ ue_on_elem(elem :T) :bool
{
elem =0
}
me hod m_is_ ue_elem ( elem :T) e u ns ( e s :bool )
{
e s := elem =0 ;
}
Finalmen e, c eamos un mé odo que a a llama al mé odo p incipal de nues o
módulo abs ac o. Hemos que ido mos a la pos condición de mane a explíci a pa a
así pode en ende mejo el p oblema que es amos esol iendo:
me hod m_all_ze o( :a ay<in >, l :in ) e u ns ( :in )
e q u i e s 1≤l≤ . Leng h
ensu es =|se p , q | 0 ≤p < q ≤ . Leng h
∧(∀k | p ≤k < q • [ k ] =0) •(p , q ) |
{
:= mcoun _seg ( ) ;
alid_segmen s_snd ( [ . . ] , 0 , . Leng h ) ;
}
5.4. P oblemas de en ana deslizan e
Pa a e mina es e capí ulo se p esen a un ipo de p oblemas de con a segmen os
en el que la longi ud del ec o es á ijada po un pa áme o adicional que se añade
al mé odo p incipal. El modelado de es e ipo de p oblemas en Da ny se p esen a
en la ca pe a /sliding_window del p oyec o.
La iloso ía que se a a segui a la ho a de p esen a es os p oblemas es la misma
que se ha seguido en an e io es secciones, pe o en es e caso de mane a más esumida,
ya que se han eu ilizado muchas de iniciones de los p oblemas de con a segmen os.
5.4.1. Modelado del p oblema
Comenzamos p esen ando la especi icación del p oblema, que es muy simila a
la de con a segmen os:
P econdición :{n≥0∧l≥1}
me hod sliding-window( [0...n), l : en e o) e u n : in
Pos condición :{ = (# p: 0 ≤p−l < p ≤n∧A( , p −l, p)}
54 Capí ulo 5. P oblemas de con a segmen os
Las unciones is_ ue_on_segmen ,we_coun ed_ ig h, alid_segmen s_ ixed_las y
alid_segmen s ealizan el mismo come ido que en los p oblemas de con a segmen os,
po lo que no se an a ol e a explica .
La di e encia p incipal es que aho a inco po amos el pa áme o l, que nos a a
pe mi i simpli ica muchos mé odos y unciones, ya que enemos que con empla
muchos menos casos. Las unciones quedan en onces de inidas de la siguien e mane a:
ghos u n c i o n we_coun ed_ ig h( :seq<T>, :i n , l :in ):bool
e q u i e s l≥1
{
=| alid_segmen s ( , 0 , | | , l ) |
}
ghos u n c i o n alid_segmen s_ ixed_las ( :seq<T>, i n i :i n , i n :in , l :in )
:se <(in ,in )>
e q u i e s 0≤ini ≤ i n ≤| |
e q u i e s l≥1
{
i ( i n −l≥ini ∧is_ ue_on_segmen ( , in −l , i n )) hen {( i n −l , i n )}
else {}
}
ghos u n c i o n alid_segmen s( :seq<T>, i n i :i n , i n :in , l :in )
:se <(in ,in )>
e q u i e s 0≤ini ≤ i n ≤| |
e q u i e s l≥1
{
i ( i n i = i n ) hen {}
else alid_segm en s ( , i n i , i n −1 , l )
+ alid_segmen s_ ixed_las ( , ini , in , l )
}
La unción min_pos_ al se man iene igual, ya que aunque a la ho a de conside a
nue os segmen os solo podemos con empla uno de ellos, el [ in - l, in), nos se -
i á pa a comp oba en iempo cons an e si debemos conside a el segmen o ac ual
pa a inc emen a .
Igual ocu e con los mé odos y el lema de inidos en la sección an e io , ealizan
la misma unción pe o aho a incluyen un nue o pa áme o ly la p econdición de
que lsea mayo o igual que uno, ya que el caso acío no se con empla. Los mé odos
y el lema quedan po an o de inidos de la siguien e mane a como se obse a en la
Figu a 5.3
Una ez modelado es e ipo de p oblemas, podemos pasa a es udia un sub ipo
conc e o de es os, y así pode inaliza la implemen ación de odas las de iniciones
que quedan pendien es en el módulo abs ac o, excep uando aquella que depende
de la p opiedad conc e a.
5.4.2. P opiedades uni e sales sob e elemen os
En es a sección p esen amos los p oblemas simila es a los es udiados en las sec-
ciones homólogas de los o os ipo de p oblemas, pe o aho a adap ando nues as so-
luciones a las ca ac e ís icas conc e as de nues o p oblema. El modelado en Da ny
explicada en es a subsección, se encuen a en el módulo SlidingWindowFo AllP en el
5.4. P oblemas de en ana deslizan e 55
me hod a iable_ini ializa ion( :a ay<T>, l :in )
e u ns ( :in , k :i n , n :in )
e q u i e s 1≤l≤ . Leng h
ensu es 0≤k≤n≤ . Leng h
ensu es =| alid_segmen s ( [ . . ] , 0 , n , l ) |
ensu es k=min_pos_ al ( [ . . ] , 0 , n)
me hod upda e_seg_coun
( :a ay<T>, :i n , old_limi :in , k :i n , l :in )
e u ns (new_ :in )
e q u i e s 0≤o l d _ l i m i < . Leng h
e q u i e s l≥1
e q u i e s k=min_pos_ al ( [ . . ] , 0 , o l d _ l i m i + 1)
e q u i e s =| alid_segmen s ( [ . . ] , 0 , o ld_limi , l ) |
ensu es new_ =| alid _s eg me n s ( [ . . ] , 0 , o l d _ l i m i + 1 , l ) |
me hod upda e_lowe _limi
( :a ay<T>, i n i :in , old_lw :in , new_up :in )
e u ns (new_lw :in )
e q u i e s 0≤ini ≤old_lw < new_up ≤ . Leng h
e q u i e s old_lw =min_pos_ al ( [ . . ] , i n i , new_up −1)
ensu es 0≤new_lw ≤new_up
ensu es new_lw =min_pos_ al ( [ . . ] , i n i , new_up)
me hod mcoun _seg ( :a ay<T>, l :in )
e u ns ( :in )
e q u i e s 1≤l≤ . Leng h
ensu es we_coun ed_ ig h ( [ . . ] , , l )
lemma alid_segmen s_snd ( :seq<T>, i n i :i n , i n :in , l :in )
e q u i e s 0≤ini ≤ i n ≤| |
e q u i e s l≥1
ensu es al id _s eg men s ( , i n i , i n , l ) =se p | i n i ≤p−l < p ≤ i n
∧is_ ue_on_segmen ( , p −l , p ) •( p −l , p )
Figu a 5.3: P incipales mé odos y lemas pa a los p oblemas de en ana deslizan e.
iche o /sliding_window/uni a y.pd .
El módulo en cues ión e ina el módulo abs ac o SlidingWindow po lo que las
unciones y mé odos son los mismos que los explicados en la an e io subsección. En
es e caso el in a ian e es el mismo que en el caso de con a segmen os, al ene el
lími e in e io ijo.
Como en o as secciones, lo p ime o que de inimos es una unción is_ ue_on_elem
que se e encia á en la implemen ación del is_ ue_on_segmen . Quedan así de inidos
las unciones. Cada unción iene acompañada de su espec i o mé odo, pa a man-
ene la sepa ación en e implemen ación y especi icación. Si no man u iésemos la
a iable ken el mé odo p incipal, nos e íamos obligados a inclui ambién un mé o-
do m_is_ ue_on_segmen como el que se mues a en la Figu a 5.4, lo que p o oca ía
que el cos e en iempo de nues o algo i mo uese cuad á ico. Es e mé odo se ía
necesa io en caso de ene que comp oba la p opiedad en odo el segmen o, pe o
es o no ocu e pa a el ipo de p opiedades al que nos es amos es ingiendo.
Aho a que hemos de inido las unciones que an a egi nues o modelo y algún
mé odo asociado, podemos pasa a implemen a los mé odos p incipales, que como
ya se ha explicado, son los mismos que en el caso de con a segmen os.
56 Capí ulo 5. P oblemas de con a segmen os
me hod m_is_ ue_on_segmen ( :a ay<T>, i n i :i n , i n :in )
e u ns ( e s :bool )
e q u i e s 0≤ini ≤ i n ≤ . Leng h
ensu es e s =is_ ue_on_segmen ( [ . . ] , i n i , i n )
{
a cond , aux , i := ue , ue , i n i ;
while i < i n ∧cond
in a ian i≤ i n
in a ian cond =is_ ue_on_segmen ( [ . . ] , i n i , i )
{
aux := m_is_ ue_elem ( [ i ] ) ;
cond := cond ∧aux ;
i:= i + 1 ;
}
e s := cond ;
}
Figu a 5.4: Ejemplo de m_is_ ue_on_segmen ine icien e.
El p ime o de ellos es a iable_ini ializa ion, en es e caso pedimos como p e-
condición que la longi ud del ec o sea mayo que l. Reco emos los p ime os l
elemen os pa a comp oba si se cumple la p opiedad pa a es e p ime segmen o,
debemos eco e lo en e o, pues ambién es amos calculando el alo k. El mé odo
queda implemen ado como apa ece en la Figu a 5.5.
El mé odo upda e_seg_coun simplemen e comp ueba si el nue o posible segmen o,
[n - l, n) cumple la p opiedad, pa a ello comp ueba si el lími e in e io del segmen o
es mayo o igual que k, y ac ualiza el con ado en consecuencia. La implemen ación
del mé odo se puede obse a en la Figu a 5.6.
El mé odo upda e_lowe _limi es igual que su homólogo de con a segmen os, po
lo que no lo p esen amos. Finalmen e p esen amos el mé odo p incipal, que sigue el
mismo esquema que en casos an e io es:
me hod mcoun _seg ( :a ay<T>, l :in ) e u ns ( :in )
{
a n:in , k :in ;
, k , n := a iable_ini ializa ion( , l );
while n < . Leng h
in a ian 0≤k≤n≤ . Leng h
in a ian k=min_pos_ al ( [ . . ] , 0 , n)
in a ian =| alid_segmen s ( [ . . ] , 0 , n , l ) |
{
min_pos_ al_snd ( [ . . ] , 0 , n + 1 ) ;
k:= upda e_lowe _li mi ( , 0 , k , n + 1 ) ;
:= upda e_seg_coun ( , , n , k , l ) ;
n:= n + 1 ;
}
}
Pa a e mina la subsección, p esen amos algunos lemas auxilia es que son de
u ilidad a la ho a de lle a a cabo la e i icación. Se p esen an las de iniciones en la
Figu a 5.7. Todos es os lemas han sido demos ados en el módulo desc i o, así como
5.4. P oblemas de en ana deslizan e 57
me hod a iable_ini ializa ion( :a ay<T>, l :in )
e u ns ( :in , k :i n , n :in )
{
n:= l ;
alid_segmen s_sho e _ han_l( [..] , 0, n −1 , l ) ;
:= 0; k := 0 ;
a cond , aux , i := ue , ue , 0 ;
while i < n
in a ian k≤i≤n
in a ian cond =is_ ue_on_segmen ( [ . . ] , 0 , i )
in a ian k=min_pos_ al ( [ . . ] , 0 , i )
{
aux := m_is_ ue_elem ( [ i ] ) ;
cond := cond ∧aux ;
i (¬aux ) { k := i + 1; }
i:= i + 1 ;
}
i ( cond ) { := 1; }
}
Figu a 5.5: Implemen ación de a iable_ini ializa ion pa a en ana deslizan e
aquellos de inidos y no demos ados en el módulo abs ac o.
5.4.2.1. Ejemplo
Como en módulos an e io es, p esen amos un ejemplo del ipo de p oblemas que
podemos esol e haciendo uso de es e módulo. La implemen ación que se mues a
puede encon a se en el módulo Tes SlidingWindow que se encuen a en el iche o
code/sliding_window/ es .d y.
P oblema. Dado un ec o , que emos conoce el núme o de segmen os de una lon-
gi ud ija lque cumplen que odos sus elemen os son pa es. Se supone que el ec o
p opo cionado iene una longi ud de, al menos, l.
Como en o os casos, lo p ime o que enemos que de ini son la unción is_ ue_-
on_elem y el mé odo m_is_ ue_elem. También ijamos el ipo de los ec o es con los
que es amos abajando. Se mues an en la Figu a 5.8.
Y aho a ya podemos implemen a el siguien e mé odo p incipal, que apa ece en
la Figu a 5.9.

58 Capí ulo 5. P oblemas de con a segmen os
me hod upda e_seg_coun
( :a ay<T>, :i n , old_limi :in , k :i n , l :in )
e u ns (new_ :in )
{
a new_limi := old_limi + 1;
new_ := ;
min_pos_ al_limi s ( [ . . ] , 0 , new_limi ) ;
min_pos_ al_snd ( [ . . ] , 0 , new_limi ) ;
no_need_ o_come_back ( [ . . ] , 0 , new_limi ) ;
i ( new_limi −l≥0){
a cond := k≤new_limi −l ;
i ( cond ) {
new_ := + 1 ;
alid_segmen s_second ( [ . . ] , 0 , old_limi , l ) ;
}
}
}
Figu a 5.6: Implemen ación de upda e_seg_coun pa a en ana deslizan e.
lemma alid_segmen s_second( :seq<T>, i n i :i n , i n :in , l :in )
e q u i e s 0≤ini ≤ i n < | |
e q u i e s l≥1
ensu es ∀p , q | ( p , q ) i n ali d_ se gmen s ( , i n i , i n , l ) •q≤ i n
lemma alid_segmen s_ ixed_las _sho e _ han_l
( :seq<T>, i n i :i n , i n :i n , l :in )
e q u i e s 0≤ini ≤ i n ≤| |
e q u i e s l≥1∧( i n −l ) < i n i
ensu es alid_segmen s_ ixed_las ( , ini , in , l ) ={}
lemma alid_segmen s_sho e _ han_l
( :seq<T>, i n i :i n , i n :i n , l :in )
e q u i e s 0≤ini ≤ i n ≤| |
e q u i e s l≥1∧( i n −i n i ) < l
ensu es al id _s eg men s ( , i n i , i n , l ) ={}
lemma alid_segmen s_snd ( :seq<T>, i n i :i n , i n :in , l :in )
lemma min_pos_ al_limi s ( :seq<T>, i n i :in , i n :in )
e q u i e s 0≤ini ≤ i n ≤| |
ensu es ini ≤min_pos_ al ( , i n i , i n ) ≤ i n
lemma min_pos_ al_snd ( :seq<T>, i n i :in , i n :in )
e q u i e s 0≤ini ≤ i n ≤| |
e q u i e s ini ≤min_pos_ al ( , i n i , i n ) ≤ i n
ensu es is_ ue_on_segmen ( , min_pos_ al ( , i n i , i n ) , i n )
lemma closed_on_le _lemma()
ensu es ∀i n i , i n , p , s :seq<T> | 0 ≤ini ≤p≤ i n ≤|s| ∧
is_ ue_on_segmen ( s , i n i , i n ) •is_ ue_on_segmen ( s , i n i , p )
lemma no_need_ o_come_back ( s :seq<T>, i n i :in , i n :in )
e q u i e s 0≤ini ≤ i n ≤|s|
ensu es ∀p:in | i n i ≤p < min_pos_ al ( s , i n i , i n ) ≤ i n
• ¬is_ ue_on_segmen ( s , p , i n )
Figu a 5.7: Lemas pa a p opiedades uni e sales en en ana deslizan e
5.4. P oblemas de en ana deslizan e 59
ype T = in
ghos u n c i o n is_ ue_on_elem(elem :T) :bool
{
elem % 2 =0
}
me hod m_is_ ue_elem ( elem :T) e u ns ( e s :bool )
{
e s := elem % 2 =0;
}
Figu a 5.8: Especi icación e implemen ación de la p opiedad en el ejemplo de en ana
deslizan e.
me hod m_all_ze o( :a ay<in >, l :in ) e u ns ( :in )
e q u i e s 1≤l≤ . Leng h
ensu es =|se p | 0 ≤p−l < p ≤ . Leng h
∧(∀k | p −l≤k < p • [ k ] % 2 =0) •( p −l , p ) |
{
:= mcoun _seg ( , l ) ;
alid_segmen s_snd ( [ . . ] , 0 , . Leng h , l ) ;
}
Figu a 5.9: Ejemplo de en ana deslizan e donde odos son pa es.
Cap´
ı ulo 6
Conclusiones y T abajo Fu u o
En es e capí ulo se a a á de esumi el abajo lle ado a cabo du an e el desa-
ollo del p oyec o, las conclusiones a las que se ha llegado con espec o a las me as
p opues as al inicio, las di icul ades encon adas y posible líneas de abajo u u o.
Con espec o a las me as que se p opusie on al p incipio del p oyec o, se ha
lle ado a cabo con éxi o la esolución de bas an es de ellas, mien as que o as han
quedado en el in e o. Se ha conseguido abs ae di e en es ipos de p oblemas sob e
segmen os, y se han e i icado u ilizando la he amien a Da ny, pe o en un inicio se
p opusie on más ipos de p oblemas que no se han podido llega a abo da .
Po lo an o, una de las posibles líneas pa a con inua abajando en es e ema
en un u u o se ía p ecisamen e a a de abo da los ipos de p oblemas que no se
han a ado, que son los mencionados en la Sección 3.4.
O a de las posible líneas de in es igación se ía segui es udiando los p oblemas
de es e abajo. No hemos con emplado a a po sepa ado p opiedades cuya p o-
piedad ue a exclusi amen e ce ada po la de echa, ya que se ha conside ado que
se llega ía a esul ados simila es. Tampoco se ha p o undizado como un caso apa e
en el caso de p opiedades que son disyunciones de o as p opiedades más simples.
Un ejemplo de es e ipo de p oblemas se ía la p opiedad que comp ueba si el p o-
duc o de los elemen os del segmen o es posi i a, pa a esol e lo de mane a i e a i a
debemos ene en cuen a dos p opiedades, que el núme o de posi i os y el núme o
de nega i os del segmen o en cu so. Es e ejemplo apa ece en el p oblema 23 del
Capí ulo 4del lib o Algo i mos co ec os y e icien es [11].
Pa a inaliza , oy a desc ibi las di icul ades que he encon ado y los conoci-
mien os que he adqui ido.
La e i icación o mal de p og amas es un campo al que me sen ía a aído an es
de comenza es e abajo, y es po eso que elegí es e ema pa a mi p oyec o de in de
ca e a. Cabe deci que an es de es e abajo nunca había enido que en en a me
a es a o ma de c ea código, ya que asigna u as an e io es (como Fundamen os de
Algo i mia) se me había animado a plan ea los p oblemas siguiendo la ó mula de
p econdición-pos condición, pe o nunca había a ado de demos a la co ección de
mis algo i mos.
61