Verificación de algoritmos sobre segmentos de un vector utilizando módulos abstractos en Dafny

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