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

Verificación de algoritmos sobre segmentos de un vector utilizando módulos abstractos en Dafny Verification of algorithms on array slices using abstract modules in Dafny Trabajo de Fin de Grado Curso 2023–2024 Autor Pablo Martín Viñuelas Directora Clara María Segura Díaz Doble Grado en Matemáticas e Ingeniería Informática Facultad de Informática Universidad Complutense de Madrid Verificación de algoritmos sobre segmentos de un vector utilizando módulos abstractos en Dafny Verification of algorithms on array slices using abstract modules in Dafny Trabajo de Fin de Grado en Ingeniería Informática Autor Pablo Martín Viñuelas Director Clara María Segura Díaz Convocatoria: Junio 2024 Doble Grado en Matemáticas e Ingeniería Informática Facultad de Informática Universidad Complutense de Madrid 26 de mayo de 2024 Resumen Verificación de algoritmos sobre segmentos de un vector utilizando módulos abstractos en Dafny La verificación formal de programas permite expresar y comprobar las propiedades que cumplen los programas. El objetivo de este proyecto es el de verificar algoritmos que computan información sobre los segmentos de un vector, como por ejemplo el segmento más largo que cumple una propiedad o el número de segmentos que cumple una propiedad. En primer lugar, se introducirá la herramienta Dafny, un lenguaje de programación que utiliza un resolutor SMT para comprobar las condiciones de verificación necesarias introducidas por el usuario. En segundo lugar, se llevará a cabo una explicación de los algoritmos con los que vamos a trabajar y algunos ejemplos concretos de su aplicación. Posteriormente, se modelizarán este tipo de problemas en Dafny, para poder así llevar a cabo la implementación del algoritmo en la herramienta, con el fin de finalmente verificar que cumple las propiedades que esperamos de las soluciones. Se tratará de presentar cada problema con diferentes niveles de abstracción, es decir, para cada problema se presentarán diferentes soluciones dependiendo del tipo de propiedades que se estén comprobando sobre los segmentos. De esta forma, para determinados casos obtendremos soluciones más eficientes. Palabras clave verificación, Dafny, algoritmia, verificación asistida. v Abstract Verification of algorithms on array slices using abstract modules in Dafny Formal verification techniques allow us to express and check the properties that programs meet. The purpose of this project is to verify algorithms that compute information concerning the segments of a vector, such as the longest segment that holds a property or the number of segments that hold a certain property. Firstly, we introduce the tool we have used, Dafny. It is a programming language that uses a SMT solver to check whether or not the verification conditions specified by the user are fulfilled. Secondly, we will deepen into the algorithms we have studied and some concrete examples. Later we will model those problems using Dafny so that we are able to verify that the algorithm implementation verifies the properties we expect. We will present each kind of problem with different levels of abstraction. To each kind of problem we will present different solutions depending on the type of property being checked on segments. This way, we will obtain more efficient solutions to some specific cases. Keywords verification, Dafny, algorithmics, assisted verification vii Índice 1. Introducción 1 1.1. Objetivos ................................. 1 1.2. Plandetrabajo.............................. 2 2. Dafny 5 2.1. Especificación e implementación . . . . . . . . . . . . . . . . . . . . . 5 2.1.1. Implementación y métodos . . . . . . . . . . . . . . . . . . . . 7 2.1.2. Especificación y funciones . . . . . . . . . . . . . . . . . . . . 8 2.1.3. TiposenDafny .......................... 9 2.1.4. Módulos.............................. 10 3. Algoritmos para el procesamiento de segmentos 15 3.1. Definiciones y conceptos . . . . . . . . . . . . . . . . . . . . . . . . . 15 3.2. Esquema general de algoritmos iterativos . . . . . . . . . . . . . . . . 16 3.3. Tipos de problemas contemplados . . . . . . . . . . . . . . . . . . . . 17 3.3.1. Problemas de segmentos de longitud máxima . . . . . . . . . . 17 3.3.2. Problemas de contar segmentos . . . . . . . . . . . . . . . . . 18 3.4. Otrosproblemas.............................. 20 4. Problemas de segmentos de longitud máxima 21 4.1. Modelización del problema . . . . . . . . . . . . . . . . . . . . . . . . 22 4.2. Demostración de la corrección . . . . . . . . . . . . . . . . . . . . . . 26 4.3. Abstracción y concreción sobre los problemas . . . . . . . . . . . . . . 27 4.3.1. Propiedades cerradas por la izquierda . . . . . . . . . . . . . . 28 4.3.2. Propiedades universales sobre elementos . . . . . . . . . . . . 29 ix Cap´ ıtulo 2 Dafny Dafny es una herramienta diseñada para la verificación de software mediante el paradigma de “Correcto por Construcción”. Está compuesto por un lenguaje de programación y mecanismos que permiten la especificación de programas. Dafny, [4] está diseñado para permitir paralelamente el desarrollo de código y una demostración de su corrección. Dafny considera que un programa es correcto si este termina y satisface la especificación proporcionada. Para alcanzar este objetivo, el usuario deberá proporcionar una especificación sobre el comportamiento que se espera del programa. Este proceso se lleva a cabo mediante el uso de precondiciones y postcondiciones, que son propiedades que deberán ser verificadas antes y después de la ejecución de cada uno de los métodos, funciones y lemas. Dafny fue creado por Rustan Leino para Microsoft Research, y se ha utilizado en diferentes proyectos, como por ejemplo para la verificación del AWS Encryption SDK, [6] y para la especificación y verificación de la red Eth2.0, [3]. El lenguaje combina ideas de los paradigmas imperativo y funcional, y puede ser compilado a otros lenguajes como Java, C#, JavaScript o Python. Para comprobar las demostraciones, Dafny hace uso del demostrador automático de teoremas Z3 a través del lenguaje intermedio Boogie. En este capítulo se introducen algunos conceptos importantes de Dafny. Será de especial importancia introducir los mecanismos que nos proporciona Dafny para llevar a cabo la especificación y verificación. También se presentarán conceptos como módulos o tipos que serán utilizados también en nuestro proyecto. Se ha tomado como referencia el capítulo homólogo de Paula Pastor Pérez en su Trabajo Fin de Master Verification of Greedy Algorithms in Dafny [9]. 2.1. Especificación e implementación Dado que el objetivo de Dafny es el de llevar a cabo de manera paralela la especificación y la implementación de los programas, es importante mantener una 5 6Capítulo 2. Dafny separación entre estos dos mundos para así conseguir un código más legible y sencillo de comprender. Aquí juega un papel importante la combinación que encontramos en Dafny de los paradigmas imperativo y funcional. Con el primero es con el que vamos a implementar nuestros programas, haciendo uso de métodos y de estructuras de datos, como los array, que contemplan los efectos laterales, mientras que con el segundo llevaremos a cabo la especificación mediante funciones y estructuras de datos, como las secuencias, que no permiten los efectos laterales. Para poder conectar ambos mundos, nos valemos de las cláusulas requires yensures que representan las ya mencionadas precondiciones y postcondiciones. Estas cláusulas se escriben debajo de la cabecera de los métodos, funciones y lemas. Dafny asume que la precondición siempre se cumple al inicio de la ejecución del método, función o lema. Es por esto que si tratamos de hacer una llamada a un método (o función o lema), Dafny comprobará si se cumple la precondición antes de ejecutar el cuerpo, y devolverá error en caso contrario. Por otro lado, las clausulas ensures especifican una propiedad que ha de cumplirse al finalizar el método (o función o lema). La ausencia de precondiciones o postcondiciones se corresponde con las cláusulas requires true yensures true, respectivamente. La primera de ellas es trivialmente cierta, mientras que la segunda simplemente nos asegura la terminación. Nuestros métodos serán especificados mediante funciones recursivas que utilizaremos en las precondiciones y postcondiciones de los mismos, y contendrán la implementación de nuestro programa. Para poder verificar que los métodos alcanzan la postcondición partiendo de la precondición, tendremos que probar una serie de propiedades sobre las funciones que hemos definido, este proceso se lleva a cabo mediante los lemas y asertos. Como resultado de este proceso obtenemos un método verificado en el que el usuario podrá confiar, ya que los mecanismos de Dafny le aseguran que si la entrada cumple la precondición entonces a la salida del método se alcanza la postcondición, sin necesidad de que el usuario comprenda la implementación ni la demostración de la corrección de la misma. Hasta ahora hemos descrito como podemos modelar que el programa al terminar cumple con lo que esperamos que haga, pero no podemos asegurar que termine. Con este fin Dafny nos proporciona las clausulas decreases. La clausula sirve para asegurar la terminación. Todas las funciones, métodos y bucles tiene asociada una cláusula de este tipo, aunque no aparezca de manera explícita, normalmente Dafny es capaz de inferirlas automáticamente, pero en ocasiones debemos indicarlas nosotros. Una clausula decreases está definida por una expresión, llamada medida de terminación, que es no negativa y que en cada nueva iteración o llamada recursiva, su valor decrece. En las siguientes subsecciones, nos centraremos en estudiar cómo llevar a cabo la especificación e implementación de nuestros programas, describiendo los mecanismos que nos proporciona Dafny para llevar a cabo esta tarea. Finalmente, también hablaremos de los módulos y los tipos que nos proporciona Dafny. 2.1. Especificación e implementación 7 method T r i p l e ( x :int)returns ( r :int) { var y:= 2∗x ; r:= x + y ; } Figura 2.1: Ejemplo de método Triple en Dafny 2.1.1. Implementación y métodos El objetivo de la implementación es el de generar un programa que cumpla con las expectativas del modelado. Con este fin se presentan los métodos. Un método es una sucesión de declaraciones que lleva a cabo una serie de cambios en el estado de nuestra máquina. Un ejemplo de método sería el que aparece en la Figura 2.1, encargado de calcular el triple de un valor. Este método recibe un parámetro de entrada xde tipo entero y devuelve un parámetro de salida r, que también es entero. El cuerpo del método es una serie de sentencias que en su conjunto conforma la implementación del método. Los parámetros de salida actúan como variables locales. Los parámetros de entrada pueden ser leídos pero no pueden cambiar su valor. El cuerpo de un método puede contener diferentes sentencias, como bucles o llamadas a otros métodos o lemas. Como puede verse en la Figura 2.1 no es necesario declarar el tipo de una variable cuando la declaramos, ya que Dafny es capaz de inferirlo. Para devolver un valor desde un método, debemos asignárselo al parámetro de salida. Una sentencia especial es el while. La verificación de bucles en Dafny necesita saber qué propiedades se mantienen a lo largo de las iteraciones del bucle, el invariante, para poder demostrar que se cumplen al terminar este. También necesitamos demostrar que nuestro bucle termina, para ello utilizamos una clausula decrease, aunque normalmente Dafny es capaz de verificarlo de forma autmática. El invariante de un bucle es una propiedad que es cierta a la entrada y salida del bucle, así como en el momento de comprobar la condición de salida del bucle en cada una de las iteraciones. Para expresar nuestro invariante para un cierto bucle, utilizamos la clausula invariant. Se muestra un ejemplo en la Figura 2.2. Se trata de un programa que calcula el cociente y el resto de dividir 191 entre 7 a base de restar el divisor al dividendo hasta que el dividendo se vuelve menor que el divisor. El invariante expresa que la relación 0≤y∧7∗x+y= 191 se mantiene a lo largo de la ejecución del bucle. En ocasiones, Dafny no podrá verificar automáticamente la corrección de estas clausulas. Es por eso que utilizamos asertos, que hacemos explícitos mediante la clausula assert. Estas expresiones han de ser ciertas en cualquier momento en que la ejecución alcanza el punto en el que están definidas. Pueden ser utilizadas tanto en métodos como en lemas. Cuando Dafny no es capaz de demostrar la corrección de un aserto que sabemos es cierto, utilizamos lemas para ayudar a Dafny a concluir la propiedad deseada. Un 8Capítulo 2. Dafny var x , y := 0 , 191; while 7≤y invariant 0≤y∧7∗x+y=191 decreases y { y:= y−7; x:= x + 1 ; } a s s e r t x=191 / 7 ∧y=191 % 7; Figura 2.2: Bucle para el cálculo del cociente y módulo de 191 respecto a 7 lema es una afirmación matemática que viene acompañada de su demostración. En Dafny, un lema es muy parecido a un método: tiene un nombre, podemos añadirle parámetros, tiene precondición y postcondición y podemos llamarlo. La diferencia con los métodos es que los lemas no son considerados por el compilador, solo se tienen en cuenta durante la verificación. Para declarar un lema procedemos de la misma forma que con los métodos, pero cambiando la palabra method por lemma. 2.1.2. Especificación y funciones El objetivo de la especificación es el de describir el comportamiento de los programas que vamos a implementar. Esta especificación se lleva a cabo mediante las ya explicadas precondiciones y postcondiciones, y también a través de las funciones. Una función denota un valor computado dados unos argumentos. La propiedad que distingue a las funciones es que son deterministas, es decir, que no presentan efectos colaterales. Un ejemplo de una declaración de función en Dafny sería la que aparece en el siguiente extracto de código: function Average ( a :int , b :int):int { ( a + b ) / 2 } Nótese que, mientras un método es declarado con una serie de parámetros de salida, en su lugar una función declara el resultado en forma de tipo, y mientras que el cuerpo del método consiste en una serie de instrucciones, el cuerpo de una función es una expresión. A su vez, las funciones pueden ser utilizadas en las expresiones, de manera que podemos escribir las postcondiciones como en el método siguiente: method T r i p l e ( x :int)returns ( r :int) ensures Average ( r , 3 ∗x ) =3∗x El código anterior saca a relucir otra diferencia importante entre métodos y funciones en Dafny. Mientras que los métodos son opacos, las funciones son transparentes. Esto quiere decir que Dafny no entiende una función solo como la pareja 2.1. Especificación e implementación 9 de su precondición y postcondición, sino que también conoce su cuerpo a la hora de razonar sobre sus propiedades. Cuando razonamos sobre un programa, es bastante común necesitar más información de la que necesita el compilador. Por esta razón, una declaración, variable, función, etc. que se utiliza solo en el contexto de la verificación, se denomina ghost. El verificador tiene en cuenta a los ghost, pero no así el compilador, que los elimina cuando genera el código compilado. Nosotros utilizaremos funciones ghost o fantasma para modelar el comportamiento de nuestro programa, estas funciones desaparecerán durante la compilación pero nos servirán para razonar sobre el comportamiento que se espera de los métodos. Un ejemplo de esta forma de razonar aparece en el siguiente extracto de código: ghost f u n c t i o n fibonacci(n :nat ):nat decreases n { i f ( n =0∨n=1) then n else fibonacci(n −1) + f i b o n a c c i ( n −2) } method m_fibonacci(n :int)returns ( f :int) r e q u i r e s n≥0 ensures f=f i b o n a c c i ( n) 2.1.3. Tipos en Dafny Los tipos en Dafny se clasifican en valor y referencia. Los primero son aquellos que están definidos por tipos escalares básicos (int,nat,bool...) y agrupaciones de los anteriores (seq,set,multiset...). Estos tipos son inmutables. Para cualquier tipo T, cada uno de los valores de tipo set<T> es un conjunto finito de valores del tipo T. Un conjunto está formado por una colección de elementos del mismo tipo, sin repeticiones y sin un orden concreto. El conjunto vacío se expresa con {}. Dafny presenta una notación alternativa para definir conjuntos, utilizando set comprehension. La siguiente notación: set x: T | p(x) :: f(x) nos devuelve el conjunto de los elementos f(x) tales que se cumple p(x). La notación |s| nos devuelve el tamaño del conjunto. Mostramos a continuación algunos ejemplos: var s:= {1 , 2 , 3 , 4} ; var t:= {2 , 3 ,4 , 1}; a s s e r t s=t ; El tipo que vamos a utilizar para representar segmentos en nuestras funciones y lemas es la secuencia (seq<T>) donde Trepresenta el tipo de los elementos contenidos en los segmentos con los que estamos trabajando. En este caso los elementos sí están ordenados, al tener todos ellos un índice asociado. Podemos extraer elementos de la secuencia utilizando índices (s[i]) y cortes (s[lo..hi]), en el primer caso se devuelve el elemento en cuestión, mientras que el segundo se obtiene una nueva secuencia formada por el resultado de tomar los primeros hi elementos y desechar los lo 10 Capítulo 2. Dafny primeros. La longitud de una secuencia (v)la podemos obtener mediante la notación |v|. Podemos observar algunos ejemplos de este tipo de datos a continuación: var s:= [ 1 , 2 , 3 , 4 ] ; a s s e r t s[2..4] =[3 , 4 ] ; a s s e r t |s| =4 ; Existen otros tipos inmutables como los multiset,string ymap, pero no vamos a profundizar en ellos ya que no los vamos a utilizar en nuestro trabajo. Además de los tipos valor que hemos explicado, Dafny también presenta los tipos referencia. En este grupo se encuadran las class y los array. Estos tipos sí son mutables. En este trabajo solo se han utilizado array, por lo que nos centraremos en explicar este tipo. Los array de Dafny son de tamaño fijo y se almacenan en el heap. Para obtener la longitud de un array (a) dado, podemos utilizar la notación a.Length que nos devuelve la longitud en forma de número natural. De manera análoga a las secuencias, podemos utilizar índices para acceder a los elementos del array. De manera adicional, podemos convertir los array a secuencias, utilizando la notación que aparece en el siguiente código: var a:= new i n t [ 3 ] a s s e r t a . Length =3 ; a [ 0 ] , a [ 1 ] , a [ 2 ] := 6 , 28 , 496; var s:= a[1..3] a s s e r t s=[ 28 , 496] Si no especificamos los índices en la anterior notación, es decir a[..], la secuencia resultante contendrá a todo el array. Además de lo anterior, Dafny nos permite representar pares de elementos, no necesariamente del mismo tipo. Si quisiéramos agrupar dos elementos, el primero (t) de tipo Ty el segundo (u) de tipo U, podemos obtener un elemento de tipo (T, U) mediante el constructor (t, u). Para acceder al primer elemento de un par p, utilizamos el destructor p.0, e igual para el segundo, utilizaremos p.1. Como apunte final respecto a los tipos, debemos hablar de la estructura de datos que hemos utilizado para representar los segmentos. En los métodos, el vector viene dado por un array del tipo con el que se esté trabajando, mientras que en las funciones y lemas nos valemos de secuencias. Esta decisión se toma con el objetivo de mantener separadas la implementación y la especificación. 2.1.4. Módulos La abstracción y la ocultación de información son aspectos necesarios en un buen diseño de programas, ya que nos permiten manejar de forma más sencilla las complejas relaciones entre las distintas partes de nuestro programa. Los módulos 2.1. Especificación e implementación 11 nos permiten agrupar tipos, métodos, funciones y otros módulos, que guardan cierta relación entre ellos. Nosotros vamos a utilizar dos tipos de sentencias sobre módulos en nuestro trabajo: la definición y la importación. Cuando definimos nuevos módulos, utilizamos la palabra reservada module, seguida del nombre del módulo y el cuerpo del mismo. En el cuerpo podemos incluir métodos, funciones, lemas, otros módulos, etc. Todos los elementos definidos dentro de un módulo están disponibles para su uso por otros elementos del módulo, pero no así para aquellos fuera del módulo. Si queremos importar los elementos de otro módulo, podemos hacerlo mediante la palabra reservada import seguida del nombre del módulo. Si queremos evitar tener que hacer referencia a los elementos del otro módulo con el nombre del módulo precediendo el del elemento, podemos utilizar import opened, pero debemos evitar conflictos entre ambos módulos. De vital importancia para nuestro proyecto son los módulos abstractos y el refinamiento de los mismos. Los primeros son módulos que presentan métodos, funciones o lemas sin implementar y será en los módulos que refinarán a estos donde implementaremos estos métodos, funciones o lemas. Los módulos abstractos no son compilados y se declaran precediendo la definición del módulo con la palabra reservada abstract. Un módulo que refina a otro es un módulo que incluye todas las propiedades, definiciones, métodos o lemas del primero, añadiendo elementos adicionales para una mayor particularización. Podemos observar ejemplos de lo explicado en las Figuras 2.3 y 2.4. Estos ejemplos se han extraído del trabajo fin de máster: Verification of greedy algorithms in Dafny [9] y representan la estructura matemática de grupo y de grupo aditivo de enteros, este segundo como refinamiento del primero. 12 Capítulo 2. Dafny a b s t r a c t module Group { type G function Product(x :G, y :G) :G lemma Associativity(x :G, y :G, z :G) ensures Product(x , Product(y , z)) =Product ( Product ( x , y ) , z ) function I d e n t i t y ( ) :G lemma IdentityIsNeutral(x :G) ensures Product ( x , I d e n t i t y ( ) ) =x ensures Product ( I d e n t i t y ( ) , x ) =x function Inverse(x :G) :G lemma ProductInverse(x :G) ensures Product ( x , I n v e r s e ( x )) =I d e n t i t y ( ) ensures Product ( I n v e r s e ( x ) , x ) =I d e n t i t y () lemma S i m p l i f y L e f t ( a :G, b :G, c :G) r e q u i r e s Product ( a , b ) =Product ( a , c ) ensures b=c { calc { Produc t ( a , b ) =Product ( a , c ) =⇒ Product ( I n v e r s e ( a ) , Product ( a , b )) =Product ( I n v e r s e ( a ) , Product ( a , c ) ) ; =⇒{ A s s o c i a t i v i t y ( I n v e r s e ( a ) , a , b ) ; A s s o c i a t i v i t y ( I n v e r s e ( a ) , a , c ) ; } Product ( Product ( I n v e r s e ( a ) , a ) , b ) =Product ( Product ( I n v e r s e ( a ) , a ) , c ) ; =⇒{ P r o d u c t I n v e r s e ( a ) ; } Product ( I d e n t i t y ( ) , b ) =Product ( I d e n t i t y ( ) , c ) ; =⇒{ IdentityIsNuetral(b); IdentityIsNeutral(c); } b=ca ; } } } Figura 2.3: Módulo abstracto que representa la estructura de grupo 2.1. Especificación e implementación 13 module AdditiveInt refines Group { type G = int function Product(x:G, y :G) :G { x+y } lemma Associativity(x :G, y :G, z :G) ensures Product(x , Product(y , z)) =Product ( Product ( x , y ) , z ) {} function I d e n t i t y ( ) :G { 0 } lemma IdentityIsNeutral(x :G) ensures Product ( c , I d e n t i t y ( )) =x ensures Product ( I d e n t i t y ( ) , x ) =x {} function Inverse(x :G) :G { −x } lemma ProductInverse(x :G) ensures Product ( x , I n v e r s e ( x )) =I d e n t i t y ( ) ens ur s Product ( I n v e r s e ( x ) , x ) =I d e n t i t y ( ) {} } Figura 2.4: Módulo concreto que refina la estructura de grupo para los enteros. 20 Capítulo 3. Algoritmos para el procesamiento de segmentos int n = l; int r = 0; int s = 0; while (n < v. size ()) { if (!(v[n] % 2 == 0)) { s = n + 1; } if(n + 1 - l >= 0 && s <= n + 1 - l) { r++; } ++n; } Figura 3.4: Algoritmo para contar cuántos segmentos de longitud lcumplen que todos sus elementos son pares {r= (# p: 0 ≤p−l < p ≤ |v|:A(v, p −l, q)} Y, de manera similar a los anteriores problemas, nuestro invariante es: {r= (# p: 0 ≤p−l < p ≤n:A(v, p −l, q)} De esta forma, cuando nuestro bucle finalice, habremos alcanzado la postcondición. 3.4. Otros problemas Otros problemas que no hemos podido estudiar sin: Existe un subsegmento que cumple una propiedad. Para todo subsegmento se cumple una propiedad. Subsegmento que cumple una propiedad tal que la suma de sus elementos es máxima. Cabe decir que que los dos primeros problemas son realmente uno solo, ya que comprobar si todos los subsegmentos de un vector cumplen una propiedad Aes equivalente a comprobar que no existe ningún segmento que cumple el contrario de la propiedad A. Estos problemas se resuelven recorriendo el vector de un extremo a otro, en el primer caso buscando el segmento que cumple Ay en el segundo el segmento que no cumple A, en ambos casos si encontramos dicho segmento se detiene la búsqueda al haber hallado la respuesta al problema. Cap´ ıtulo 4 Problemas de segmentos de longitud máxima En este capítulo se profundizará en la que ha sido la parte fundamental del proyecto, el estudio de la verificación de los problemas de cálculo del segmento de longitud máxima que cumple una propiedad dado un vector de elementos. Todo el modelado y verificación de estos problemas en Dafny se encuentra en la carpeta seg-long-max del proyecto. Durante el desarrollo del proyecto se han estudiado diferentes problemas y sus respectivas soluciones. Se han encontrado similitudes y diferencias entre los distintos problemas, existiendo para algunos casos concretos algoritmos más eficientes que el caso general para su solución, debido principalmente a las características y formato de las propiedades que han de cumplir los segmentos. Es por esto que se hace necesario una clasificación por casos dentro de este tipo de problemas, así como una abstracción común que agrupe las similitudes a la hora de resolver cada uno de ellos. De esta forma un usuario elegirá el módulo más apropiado para resolver su problema y en muchos casos bastará con que proporcione los detalles más específicos de su problema puesto que el módulo ya contiene los elementos de verificación necesarios. La primera sección de este capítulo describe este último proceso de abstracción, mientras que la segunda describe la clasificación que se ha llevado a cabo durante el desarrollo de este trabajo. Finalmente, en la última sección de este capítulo se muestra un ejemplo que ilustra de manera concreta todo lo anterior. En la Figura 4.1 se muestra un gráfico de dependencias entre los diferentes módulos que representan los diferentes tipos de problemas, para una mejor comprensión por parte del lector: A continuación se ofrece una breve explicación de cada uno de ellos: SegLongMax es el módulo que abstrae las características comunes de todos los problemas de este tipo, y es del cual todos habrán de heredar. AbstractClosedLeft es el módulo que abstrae las características comunes de aquellos problemas que, además de ser del tipo de esta sección, presentan una 21 22 Capítulo 4. Problemas de segmentos de longitud máxima SegLongMax AbstractClosedLeft SegLongMaxClosedLeftSorted SegLongMaxForAllP SegLongMaxRelation Figura 4.1: Diagrama de la relación entra módulos de segmento de longitud máxima propiedad Aque es cerrada por la izquierda. SegLongMaxForAllP es el módulo que abstrae las características comunes de aquellos problemas cuya propiedad comprueba si todos los elementos del segmento cumplen una cierta propiedad. SegLongMaxRelation es el módulo que abtrae las características comunes de aquellos problemas cuya propiedad comprueba si todo los elementos del segmento cumplen una cierta relación entre cada par de ellos. SegLongMaxClosedLeftSorted es el módulo que abstrae las características comunes de aquellos problemas cuya propiedad es cerrada por la izquierda y tiene como precondición que los elementos del vector están ordenados. 4.1. Modelización del problema Las funciones y métodos descritos a continuación se encuentran en el archivo seg_long_max_abs.dfy que se encarga de abstraer aquellos métodos, funciones y lemas que son comunes a todos los problemas de este tipo. El fichero contiene un único módulo abstracto, SegLongMax, del cual refinarán todos los problemas que sean de este tipo. Estos métodos, funciones y lemas se dejan sin implementar o verificar (a excepción de algún caso concreto), ya que la manera de implementarlos eficientemente va a depender de la propiedad concreta que se esté estudiando. En las secciones siguientes se refinarán para representar distintos grupos de problemas. 4.1. Modelización del problema 23 method mseg_long_max(v :array<T>) returns ( r :int) ensures there_is_a_segment_that_long(v [..] , r ) ensures is_longest_segment(v [..] , r) ghost f u n c t i o n is_longest_segment(s :seq<T>, r :int):bool { ∀p:int , q :int | 0 ≤p≤q≤|s| ∧is_true_on_segment(s , p, q) •q−p≤r } ghost f u n c t i o n there_is_a_segment_that_long(s :seq<T>, r :int):bool { ∃p:int , q :int | 0 ≤p≤q≤|s| ∧is_true_on_segment(s , p, q) •q−p=r } Figura 4.2: Especificación del método m_seg_long_max Para empezar a explorar nuestro problema, comenzamos especificando de manera formal el mismo. Partimos de un vector vde nelementos y queremos encontrar la longitud rdel segmento que cumple una cierta propiedad Ade manera que cualquier otro segmento del vector que cumpla la propiedad presente una longitud menor o igual al rdevuelto: {n≥0} method seg-long-max(v[0...n))return r : int {r= (max p, q : 0 ≤p≤q≤n∧A(v, p, q):(q−p)} El método seglong-max que hemos especificado está representado en nuestro modelo por mseg_long_max(v : array<T>) returns (r : int). Este método tiene como parámetro el vector que está siendo estudiado y devuelve el valor rque estamos buscando. Es el método principal del algoritmo y el que se espera que el usuario utilice a la hora de modelar sus propios problemas. La postcondición que concreta las propiedades que ha de cumplir el valor que devolvemos está especificada en los predicados is_longest_segment(s : seq<T>, r : int) ythere_is_a_segment_that_long(s : seq<T>, r : int) que dados el vector y el valor devuelto, aseguran que no existe ningún segmento que cumpla la propiedad con una longitud mayor que ry que existe al menos un segmento que cumple la propiedad que tiene longitud r, respectivamente. El método queda especificado en la Figura 4.2. Observación. Nuestro método admite array genéricos, para una mayor abstracción. El tipo de los elementos lo fijará el usuario en el módulo final cuando defina la propiedad que desea estudiar. Este estándar se mantiene en todos los problemas tratados del trabajo. El que un segmento cumpla o no la propiedad viene modelado mediante la función fantasma is_true_on_segment(v : seq<T>, ini : int, fin : int) : bool que dado el vector que se está estudiando y un segmento [ini, fin), devuelve cierto si la propiedad estudiada se cumple para los elementos del segmento o falso en caso contrario. 24 Capítulo 4. Problemas de segmentos de longitud máxima La precondición de esta función es que el par (ini, fin) sean índices válidos del vector v. Nuestra forma de abordar el problema consistirá en recorrer el vector de izquierda a derecha, de manera que cuando avanzamos llevamos calculado el valor de la mayor longitud de los segmentos que cumplen la propiedad encontrados hasta el momento, este valor se almacenará en una variable r, que será el valor que terminemos devolviendo al finalizar el bucle. Además de esta variable, se utilizarán otras dos: nys, ambos valores enteros. La primera de ellas (n) representa el índice del vector antes del cual ya hemos estudiado todos los posibles segmentos, mientras que la segunda (s) representa el índice del segmento más largo tal que el segmento [s, n) cumple la propiedad. Este es el invariante que se tratará de mantener en el bucle. En cada iteración del bucle incrementaremos en uno el valor de n, el paso A2del esquema presentado en el Capítulo 3, y trataremos de mantener el invariante con respecto a las variables rys, de manera que al finalizar el mismo hayamos alcanzado la postcondición. Para poder modelar el invariante, se ha definido la función fantasma ghost function seg_long_max(v : seq<T>, ini : int, fin : int) : (int, int), definida de manera recursiva. La función devuelve dos valores enteros, el primero de ellos representa la longitud del segmento más largo que cumple la propiedad en el segmento [ini, fin) de v. El segundo de ellos representa el índice más pequeño, de manera que el segmento que delimitan este valor y fin cumpla la propiedad. Es claro que los valores que devuelve esta función están muy relacionados con las variables de program ry sque hemos definido previamente. Nótese que si llamamos a la función con los parámetros (v, 0, |v|), esta nos devuelve el rque estamos buscando. La única precondición de esta función es que (ini, fin) sean índices válidos del vector. De esta forma la función queda definida de la siguiente forma: ghost f u n c t i o n seg_long_max ( v :seq<T>, i n i :int , f i n :int):(i n t ,int) decreases f i n −ini r e q u i r e s 0≤ini ≤f i n ≤|v| La razón de existencia de esta función es la de separar el razonamiento o especificación de nuestro problema de la implementación. De esta forma, todo el razonamiento sobre las propiedades y lemas que vamos a hacer se basará en los valores devueltos por la función seg_long_max. Más adelante en la Sección 4.2 demostraremos que los valores devueltos por esta función cumplen lo expresado por la especificación dada en la Figura 4.2. Una vez definida esta función, podemos presentar el invariante concreto que llevará nuestro método principal, que no es más que asegurar que los valores de ry sque llevamos hasta el momento en nuestro recorrido por el vector se corresponden con los valores de la función se_long_max. Es decir que se cumple que: 4.1. Modelización del problema 25 while n < v . Length decreases v. Length −n invariant 0≤s≤n≤v. Length invariant r=seg_long_max ( v [ . . ] , 0 , n ) . 0 invariant s=seg_long_max ( v [ . . ] , 0 , n ) . 1 Además de lo anterior, también tenemos que asegurarnos que los valores de sy nsiempre están dentro de los límites marcados por nuestro vector, para así poder satisfacer las precondiciones de la función seg_long_max. Como función de cota se ha elegido v.Length - n. Para conseguir mantener el invariante, se han creado tres métodos más que van a ser llamados desde el principal y que representan los conjuntos de instrucciones A0y A1. El primero de ellos es el método variable_initialization(v : array<T>) returns (r : int, s: int, n : int) que se utiliza para inicializar las variables ya descritas. Este método se corresponde, por tanto, con el A0. No presenta ninguna precondición y nos asegura que los valores devueltos cumplirán el invariante en la entrada en el bucle. El método queda especificado así: method variable_initialization(v :array<T>) returns ( r :int , s :int , n :int) ensures 0≤s≤n≤v. Length ensures r=seg_long_max ( v [ . . ] , 0 , n ) . 0 ensures s=seg_long_max ( v [ . . ] , 0 , n ) . 1 También se ha especificado el método update_actual_s(v : array<T>, ini : int, old_s : int, new_k : int) returns (new_s : int) que se encarga de mantener el invariante respecto la variable s. Recibe como parámetros el vector que estamos estudiando, el índice donde se inicia el segmento que estamos estudiando [ini, new_k) , el antiguo valor de santes de que actualizase el valor de ny el nuevo valor de n, que se supone que ha incrementado en uno. Las precondiciones del método son que se cumpla el invariante para los antiguos valores de syny las postcondiciones garantizan que se mantiene. El método queda especificado de la siguiente manera: method update_actual_s(v :array<T>, i n i :int , old_s :in t , new_k :int) returns (new_s :int) r e q u i r e s 0≤ini ≤old_s < new_k ≤v. Length r e q u i r e s old_s =seg_long_max ( v [ . . ] , i n i , new_k −1 ).1 ensures 0≤new_s ≤new_k ensures new_s =seg_long_max ( v [ . . ] , i n i , new_k ) . 1 Finalmente, se especifica también el método update_actual_seg_length(v : array<T>, old_r : int, old_n : int, new_s : int) returns (new_r : int) que se encarga de mantener el invariante con respecto a la variable r. Recibe como parámetros el vector que estamos estudiando v, el antiguo valor de r, el antiguo valor de ny el nuevo valor de s. Las precondiciones del método son que se cumplan el invariante correspondiente para las variables del método principal (r, s y n), es decir, el de la iteración anterior para las variables que todavía no han sido actualizadas (old_r, old_n) y el de la actual para las actualizadas (new_s). El método queda entonces especificado como sigue: 26 Capítulo 4. Problemas de segmentos de longitud máxima method update_actual_seg_length(v :array<T>, old_r :i n t , old_n :int , new_s :int) returns (new_r :int) r e q u i r e s 0≤old_n < v . Length r e q u i r e s old_r =seg_long_max ( v [ . . ] , 0 , old_n ) . 0 r e q u i r e s new_s =seg_long_max ( v [ . . ] , 0 , old_n + 1 ) . 1 ensures new_r =seg_long_max ( v [ . . ] , 0 , old_n + 1 ) . 0 Estos dos últimos métodos se corresponden con el conjunto de instrucciones A1 del Capítulo 3. 4.2. Demostración de la corrección Una vez especificados todos estos métodos y funciones, debemos implementar aquellos que sean generales para todos los tipos de problemas y, lo más importante de todo, debemos ser capaces de conseguir que Dafny verifique nuestro código. A continuación vamos a presentar una serie de lemas que son comunes a todos los tipos de problemas que hemos estudiado y que nos van a permitir guiar a Dafny en la verificación de estos métodos. Los más importantes son los lemas: seg_long_max_existence(v : seq<T>, ini : int, fin : int) yseg_long_max_snd(v : seq<T>, ini : int, fin : int). Estos lemas se crean para permitir a Dafny deducir las postcondiciones a partir del invariante y la negación de la condición de salida de nuestro bucle, es decir, una vez terminada la ejecución del bucle. Ambos lemas reciben el vector estudiado vy los índices de inicio y fin del segmento que se está estudiando (ini, fin). La única precondición que presentan es que ambos índices estén dentro de los valores permitidos por nuestro vsean válidos. El primero de ellos, seg_long_max_existence nos asegura que existen segmentos dentro de los límites definidos en nuestro vector que cumplen la propiedad estudiada, tales que al menos uno tenga la longitud del primer valor devuelto por seg-long-max y tal que al menos exista uno que termine incluyendo el último índice del vector, y además tenga como primer índice el segundo valor devuelto por la función seg-long-max. El segundo de ellos, seg_long_max_snd nos asegura que el primer valor devuelto por la función seg-long-max es mayor o igual que la longitud de cualquier segmento que cumpla la propiedad dentro de los límites definidos por los índices pasados como parámetros. Presentamos los lemas a continuación: lemma seg_long_max_existence(v :seq<T>, i n i :int , f i n :int) r e q u i r e s 0≤ini ≤f i n ≤|v| ensures ∃p , q | i n i ≤p≤q≤f i n ∧is_true_on_segment(v , p, q) •q−p=seg_long_max ( v , i n i , f i n ) . 0 ensures ∃p | i n i ≤p≤f i n ∧is_true_on_segment ( v , p , f i n ) •p=seg_long_max ( v , i n i , f i n ) . 1 lemma seg_long_max_snd ( v :seq<T>, i n i :i n t , f i n :int) r e q u i r e s 0≤ini ≤f i n ≤|v| ensures ∀p , q | i n i ≤p≤q≤f i n ∧is_true_on_segment(v , p, q) •q−p≤seg_long_max ( v , i n i , f i n ) . 0 4.3. Abstracción y concreción sobre los problemas 27 Estos son los dos lemas que se utilizan para probar las postcondiciones dentro del método principal, pero en este módulo también se han incluido otros lemas que muestran propiedades fundamentales y útiles de la función seg-long-max y que se ha decidido incluir en el mismo, pues se utilizan mucho en cualquiera de los tipos de problemas estudiados. Además, los tres lemas nos ayudan y guían a la hora de razonar sobre cómo implementar la función seg-long-max, ya que limitan sensiblemente los posibles valores que esta puede devolver y nos orienta sobre su finalidad dentro del modelo. El primero de ellos es el lema allways_gt(s : seq<T>, fin : int) que nos asegura que el primer valor devuelto por la función seg-long-max invocada con los parámetros (s, 0, fin) es siempre mayor que la diferencia entre fin y el segundo valor devuelto por seg-long-max. La única precondición del método es que el parámetro fin sea un índice válido del vector s. Esto es así porque el primer valor del par contempla todos lo subsegmentos del vector, mientras que el segundo valor del par solo contempla aquellos cuyo extremo superior es fin. lemma allways_gt(s :seq<T>, f i n :int) r e q u i r e s 0≤f i n ≤|s| ensures seg_long_max ( s , 0 , f i n ) . 0 ≥f i n −seg_long_max ( s , 0 , f i n ) . 1 Los dos lemas restantes nos proporcionan información sobre los límites de los valores devueltos por la función seg-long-max; son seg_long_max_gt(s : seq<T>, ini : int, fin : int) yupper_limit(s : seq<T>, ini : int, fin : int). La precondición de ambos métodos es que los índices (ini, fin) con los que se invoca la función seg-long-max sean índices válidos con respecto al vector s. Esta precondición es compartida por muchos lemas, por lo que a partir de ahora solo aparecerá en el código de los lemas. El primero de ellos nos asegura que el primer valor devuelto por seg-long-max es mayor o igual que 0. El segundo nos asegura que el segundo valor devuelto por la función seg-long-max es menor o igual que el índice fin. lemma seg_long_max_gt ( s :seq<T>, i n i :in t , f i n :int) r e q u i r e s 0≤ini ≤f i n ≤|s| // Estaba e s t r i c t o ant es ensures seg_long_max ( s , i n i , f i n ) . 0 ≥0 lemma upper_limit(s :seq<T>, i n i :i n t , f i n :int) decreases f i n −ini r e q u i r e s 0≤i n i < f i n ≤|s| ensures seg_long_max ( s , i n i , f i n ) . 1 ≤f i n Una vez presentado el modelo general que seguirán todos los problemas de este tipo, podemos pasar a llevar una clasificación más exhaustiva en función de las características de las propiedades A. 4.3. Abstracción y concreción sobre los problemas En la primera sección se ha llevado a cabo una descripción de los métodos, lemas y funciones que se han utilizado en las soluciones presentadas para algoritmos 28 Capítulo 4. Problemas de segmentos de longitud máxima de segmento de longitud máxima. En esta vamos a distinguir diferentes conjuntos de problemas que comparten una serie de características comunes que nos permiten resolverlos de manera similar. Cada uno de estos subtipos de problemas refina el módulo abstracto presentado en la anterior sección y viene acompañado de un ejemplo concreto en el repositorio del trabajo. 4.3.1. Propiedades cerradas por la izquierda Nuestro trabajo se ha centrado en estudiar problemas cuyas propiedades presentasen la característica de ser cerradas por la izquierda, aunque también se muestra en el archivo test_abstract.dfy cómo implementar con nuestro modelo un problema que no presente este tipo de propiedades. Este tipo de problemas son más interesantes, pues ofrecen la posibilidad de llevar a cabo algoritmos que los solucionen de manera más eficiente, con coste en la mayor parte de los casos lineales, al contrario que si no presentasen esta propiedad, ya que en el caso general los algoritmos serán al menos de coste cuadrático, ya que deberemos estudiar todos los posibles segmentos al avanzar en uno el índice de nuestra variable n. Es por esto que, con el objetivo de presentar con mayor claridad las propiedades que distinguen estos problemas y las relaciones entre los diferentes tipos de problemas, se ha definido el módulo AbstractClosedLeft, que refina el módulo SegLongMax. En este módulo están basados todos los tipos de problemas que se presentarán a continuación. El elemento más importante que contiene el módulo es el lema closed_on_left_lemma, el cual, si se demuestra para la propiedad Aestudiada, implica que Apresenta la característica de ser cerrada por la izquierda. Se presenta a continuación: lemma closed_on_left_lemma() ensures ∀i n i , f i n , p , s :seq<T> | 0 ≤ini ≤p≤f i n ≤|s| ∧is_true_on_segment ( s , i n i , f i n ) •is_true_on_segment ( s , i n i , p ) Del lema anterior se puede deducir, aunque hay que adaptarlo a cada tipo de problema, el lema no_need_to_come_back(s : seq<T>, ini : int, fin : int) que nos asegura que para cualquier índice inferior al valor del segundo valor devuelto por la función seg-long-max, el segmento [p, fin)no puede cumplir la propiedad. El lema queda definido de la siguiente manera: lemma no_need_to_come_back ( s :seq<T>, i n i :int , f i n :int) r e q u i r e s 0≤i n i < f i n ≤|s| ensures ∀p:int | i n i ≤p < seg_long_max ( s , i n i , f i n ) . 1 ≤f i n • ¬is_true_on_segment ( s , p , f i n ) Estos lemas se dejan sin demostrar, para que sea el usuario el que, con base en la propiedad estudiada, demuestre que se cumplen. Estos lemas se demuestran de manera muy similar, ya que basta con llevar a cabo una demostración por reducción al absurdo utilizando el lema closed_on_left_lemma. 4.3. Abstracción y concreción sobre los problemas 29 Además de los lemas anteriores, presentamos una implementación común del método principal que van a compartir todos los problemas que presenten la característica de ser cerrados por la izquierda. Todos los métodos, funciones, lemas, invariantes y variables utilizados ya han sido presentados, por lo que nos limitaremos a mostrar el código del cuerpo del método principal: var n , s ; r , s , n := variable_initialization(v); while n < v . Length decreases v. Length −n invariant 0≤s≤n≤v. Length invariant r=seg_long_max ( v [ . . ] , 0 , n ) . 0 invariant s=seg_long_max ( v [ . . ] , 0 , n ) . 1 { s:= update_actual_s ( v , 0 , s , n + 1 ) ; r:= update_actual_seg_length(v, r , n, s ); n:= n + 1 ; } seg_long_max_existence ( v [ . . ] , 0 , v . Length ) ; seg_long_max_snd ( v [ . . ] , 0 , v . Length ) ; Como se puede observar, el método sigue el esquema presentado en el Capítulo 3, y podemos deducir las postcondiciones a partir de los lemas presentados. Gracias a estos lemas y a los invariantes presentados, nuestro método es aceptado por Dafny, que nos confirma su corrección. 4.3.2. Propiedades universales sobre elementos El código en Dafny de esta subsección lo podemos encontrar en el módulo SegLongMaxUnitary que refina a AbstractClosedLeft. Este módulo se encuentra en el archivo /seg-long-max/general/unitary/unitary.dfy del proyecto. Este tipo de problemas se basan en una propiedad Asobre el segmento que comprueba si para cada elemento del segmento en cuestión se cumple una cierta propiedad P. De esta forma, podemos modelar la ya definida función fantasma is_true_on_segment de la siguiente manera: ghost f u n c t i o n is_true_on_segment(v :seq<T>, i n i :int , f i n :int):bool { ∀p | i n i ≤p < f i n •is_true_on_elem(v[p]) } Debido a este formato de la propiedad A, sabemos que esta tiene dos cualidades que serán muy importantes a la hora de elegir nuestra solución: es cierta para segmentos vacíos y es cerrada por la izquierda. La función is_true_on_elem(elem : T) se deja sin implementar para que sea el usuario el que implemente la propiedad que quiera comprobar: 36 Capítulo 4. Problemas de segmentos de longitud máxima La razón por la que no se refina este módulo explícitamente es porque Dafny no permite modificar las precondiciones de métodos/funciones/lemas que estén definidas en un módulo superior, por lo que al requerir una precondición adicional, en este caso que el vector esté ordenado, se ha decidido seguir la misma estructura que en el resto de módulos pero sin hacer explícita esta relación. Este módulo se encuentra en el archivo /seg_long_max/closed_left_sorted/closed_left_sorted.dfy del proyecto. Las principales características de este módulo son, por un lado, la definición e inclusión como precondición que el vector vestudiado esté ordenado y, por otro, el alto grado de generalización, ya que las propiedades que estamos estudiando son aquellas que son propiedades sobre segmentos a las que solo les pedimos que sean cerradas por la izquierda y ciertas para el segmento vacío. En realidad, nuestro módulo serviría para modelar cualquier propiedad que sea cerrada por la izquierda y cierta para segmentos vacíos, sin necesidad de exigir que el vector esté ordenado. La razón por la que se incluye esta precondición es porque en el ejemplo que se ha elegido para representar este tipo de problemas es necesario que el vector esté ordenado para que la propiedad que se estudia sea cerrada por la izquierda, por lo que debemos incluirlo en el módulo abstracto como precondición, pues sino Dafny no nos dejaría modificar la precondición en el módulo concreto. Para modelar la propiedad que va a determinar el problema a resolver, nos valemos de la ya definida is_true_on_segment que dejamos sin implementar para que sea el usuario el que la implemente en función de la propiedad que está estudiando. De manera paralela definimos el método m_true_on_segment(v : array<T>, ini : int, fin : int) returns (res : bool) que nos va a servir para mantener la separación entre especificación e implementación, este método también se deja para que lo implemente el usuario. El nuevo método queda definido de la siguiente manera: method m_true_on_segment(v :array<T>, i n i :i n t , f i n :int)returns ( r e s :bool ) r e q u i r e s 0≤ini ≤f i n ≤v . Length ensures r e s =is_true_on_segment ( v [ . . ] , i n i , f i n ) Como este módulo engloba a todas aquellas propiedades que son cerradas por la izquierda y ciertas para segmentos vacíos, en particular es posible modelar los problemas ya descritos en los apartados anteriores. La razón para tratarlos como casos aparte es que en esos problemas es posible conseguir una solución más eficiente, ya que podemos, cuando aumentamos en uno el valor de la variable n, simplemente comprobar si se cumple una cierta propiedad PoRen los últimos elementos del vector y en caso de que no se cumpla, devolver el segmento más pequeño para el que la propiedad siempre es cierta (el vacío o el de un solo elemento). Ahora, en cambio, necesitaremos ir comprobando para cada índice pentre el antiguo valor de syfin si se cumple la propiedad para el segmento [p, fin) Esto es lo que motiva la definición de una nueva función fantasma recursiva que va a modelar este comportamiento de nuestro algoritmo, y es la que usaremos después en la especificación para definir un invariante que nos permite alcanzar la postcondición de los métodos que ya hemos definido. También la usaremos para 4.3. Abstracción y concreción sobre los problemas 37 definir y demostrar diferentes lemas que ayudarán a Dafny a llevar a cabo la verificación. Esta nueva función es update_s(v : seq<T>, ini : int, fin : int) : (int). La función recibe los mismos parámetros que su función hermana seg_long_max, y presenta la misma precondición. La función se llama desde esta función, y se utiliza para calcular el segundo valor (es decir, la variable s) en el caso en que no se cumple la propiedad para el segmento [ini, fin). La función distingue tres casos: 1. Si ini == fin entonces hemos llegado al caso vacío y, como la propiedad es cierta para segmentos vacíos, en particular es cierta para el segmento [ini, ini) por lo que devolvemos ini. 2. Si la propiedad es cierta en el segmento actual, entonces también devolvemos el valor ini. 3. En caso contrario, seguimos buscando un sadecuado, por lo que hacemos una llamada recursiva aumentando en 1el valor de ini. Cabe decir que Dafny no es capaz de definir una función de cota adecuada, por lo que se le ha proporcionado una explícita (fin - ini). Esta función de cota también será necesaria incluirla para los lemas que razonen sobre las propiedades de esta función. La función, por tanto, queda implementada de la siguiente manera: ghost f u n c t i o n update_s(v :seq<T>, i n i :i n t , f i n :int):(int) decreases f i n −ini r e q u i r e s 0≤ini ≤f i n ≤|v| { i f ( i n i =f i n ) then ini e l s e i f ( is_true_on_segment ( v , i n i , f i n ) ) then ini else update_s ( v , i n i + 1 , f i n ) } Para definir la propiedad de que un vector esté ordenado, hemos tenido que definir el predicado sorted y también fijar un tipo en este módulo abstracto, ya que en Dafny no existe un conjunto que englobe a todos los tipos comparables. Por lo tanto: type T = int ghost p r e d i c a t e s o r t e d ( s :seq<T>) { ∀p:int , q :int | 0 ≤p≤q < | s | •s [ p ] ≤s [ q ] } Para ayudarnos en la verificación, se han incluido una serie de lemas adicionales que presentamos en la Figura 4.4. La mayoría nos aportan información sobre las propiedades que cumple la nueva función que hemos definido, aunque hay algún lema nuevo sobre la función seg_long_max, pero este lo explicaremos al final de la sección con el resto de lemas anteriores. El primer lema que presentamos es update_s_limits(v : seq<T>, ini : int, fin : int) el cual nos permite asegurar que el valor de la función estará acotado por estos mismos índices. 38 Capítulo 4. Problemas de segmentos de longitud máxima lemma update_s_limits(v :seq<T>, i n i :int , f i n :int) decreases f i n −ini r e q u i r e s 0≤ini ≤f i n ≤|v| ensures ini ≤update_s ( v , i n i , f i n ) ≤f i n lemma update_s_good_segment(v :seq<T>, i n i :i n t , f i n :int) decreases f i n −ini r e q u i r e s 0≤ini ≤f i n ≤|v| r e q u i r e s ini ≤update_s ( v , i n i , f i n ) ≤f i n ensures is_true_on_segment ( v , update_s ( v , i ni , f i n ) , f i n ) lemma update_s_is_seg_long_1(v :seq<T>, i n i :i n t , f i n :int) decreases f i n −ini r e q u i r e s 0≤ini ≤f i n ≤|v| r e q u i r e s s o r t e d ( v ) ensures seg_long_max ( v , i n i , f i n ) . 1 =update_s ( v , i n i , f i n ) lemma update_s_min_value(v :seq<T>, i n i :i n t , f i n :int) decreases f i n −ini r e q u i r e s 0≤ini ≤f i n ≤|v| ensures ∀p | i n i ≤p≤f i n ∧is_true_on_segment ( v , p , f i n ) •update_s ( v , i n i , f i n ) ≤p lemma update_s_if_snd(v :seq<T>, i n i :i n t , old_s :i n t , f i n :int) r e q u i r e s 0≤i n i < f i n ≤|v| r e q u i r e s s o r t e d ( v ) r e q u i r e s ini ≤old_s ≤f i n r e q u i r e s old_s =update_s ( v , i n i , f i n −1) ensures update_s ( v , i n i , f i n ) =update_s ( v , old_s , f i n ) Figura 4.4: Propiedades de update_s para el caso cerrado por la izquierda con vector ordenado. El siguiente lema que presentamos es update_s_good_segment(v : seq<T>, ini : int, fin : int) el cual nos exige que el valor devuelto por la función update_s se encuentre acotado por (ini, fin), y nos asegura que el valor devuelto por la función forma, junto al índice fin, un segmento que cumple la propiedad. El lema update_s_is_seg_long_1(v : seq<T>, ini : int, fin : int) nos asegura que el segundo valor devuelto por la función seg_long_max es el mismo que el devuelto por la función update_s. El siguiente lema es update_s_min_value(v : seq<T>, ini : int, fin : int) el cual es muy similar al ya definido no_need_to_come_back. Dados un par de índices adecuados para nuestro vector, nos asegura que para cualquier píndice del vector vtal que la propiedad sea cierta en el segmento [p, fin) entonces sabemos que pes mayor o igual que el valor devuelto por la función update_s cuando es invocada con los parámetros que le pasamos al lema en cuestión. Finalmente, presentamos el lema update_s_if_snd(v : seq<T>, ini : int, old_s : int, fin : int) que nos asegura que si llamamos a la función update_s con los parámetros (v, ini, fin) y(v, old_s, fin) entonces nos devuelve el mismo índice. Además de estos lemas sobre la función update_s, se ha definido un nuevo lema sobre la función seg_long_max,seg_long_max_1_is_ini(v : seq<T>, ini : int, fin : int). Este lema nos exige que le proporcionemos índices (ini, fin) válidos con 4.3. Abstracción y concreción sobre los problemas 39 respecto al vector, que el vector esté ordenado y que además el segmento definido por [ini, fin) cumpla la propiedad estudiada. Si esto es cierto, entonces el lema nos asegura que el segundo valor devuelto por la función seg_long_max es el propio ini. Queda así definido: lemma seg_long_max_1_is_ini(v :seq<T>, i n i :in t , f i n :int) r e q u i r e s 0≤ini ≤f i n ≤|v| r e q u i r e s s o r t e d ( v ) r e q u i r e s is_true_on_segment ( v , i n i , f i n ) ensures seg_long_max ( v , i n i , f i n ) . 1 =ini Una vez que se han visto las nuevas funciones y lemas, veamos cómo se han implementado las ya conocidas funciones y métodos. Empecemos por la función recursiva seg_long_max. La función está definida de manera similar a los casos anteriores, de nuevo distinguimos tres casos: 1. Si ini == fin entonces nos encontramos en el caso base y como nuestra propiedad es cierta para segmentos vacíos devolvermos el par (0, ini). 2. Si nuestro segmento no cumple la propiedad entonces devolvemos como primer valor el máximo entre el segmento más largo hasta ahora y la longitud del nuevo segmento que cumple la propiedad new_s, fin y como segundo valor, como debemos actualizar s, llamamos a la función update_s(v, ini, fin). 3. Si nuestro segmento cumple la propiedad, de nuevo como primer valor devolvemos el máximo que hemos descrito en el caso en que el segmento no cumpliese la propiedad y como segundo valor devolvemos el sque llevásemos hasta ahora. La función queda por tanto implementada de la siguiente manera: ghost f u n c t i o n seg_long_max ( v :seq<T>, i n i :int , f i n :int):(i n t ,int) r e q u i r e s 0≤ini ≤f i n ≤|v| { i f ( i n i =f i n ) then (0 , i n i ) e l s e i f (¬is_true_on_segment ( v , i n i , f i n ) ) then (max( seg_long_max ( v , i n i , f i n −1 ) . 0 , f i n −update_s ( v , i n i , f i n ) ) , update_s ( v , i n i , f i n ) ) else (max( seg_long_max ( v , i n i , f i n −1 ) . 0 , f i n −seg_long_max ( v , i n i , f i n −1 ) . 1 ) , seg_long_max ( v , i n i , f i n −1).1) } Veamos ahora cómo se implementan los métodos una vez que ya se han implementado todas las funciones que van modelar su comportamiento. En el caso de variable_initialization, como de nuevo la propiedad es cierta para segmentos vacíos se implementa exactamente igual que en los casos anteriores. También el método update_actual_seg_length es muy similar a los anteriores. Es por eso que no los mostramos. Es el método update_actual_s el que cambia más con respecto a sus antecesores, ya que ahora no va a ser suficiente con comprobar una propiedad y actualizar 40 Capítulo 4. Problemas de segmentos de longitud máxima siempre al mismo índice, sino que vamos a tener que llevar a cabo un bucle en el que vamos probando uno a uno los posibles candidatos. Es en este método donde se utilizan todos los lemas definidos en este módulo, ya que debemos asegurarnos que las variables cumplen el invariante del bucle en la entrada, lo mantienen durante las iteraciones y, cuando el bucle termina, somos capaces de obtener la postcondición del método. Comenzamos asignando a una nueva variable new_s el valor del antiguo s, y en cada vuelta del bucle comprobamos si para el nueve segmento [new_s, new_n) se cumple la propiedad, si no se cumple aumentamos en 1el valor de la variable. El invariante que mantenemos en el bucle tiene dos partes, la primera que la variable new_s siempre sea menor o igual que update_s(v, old_s, new_n) y que la variable booleana cond que nos sirve para comprobar la condición del bucle se mantiene actualizada. El método queda implementado de la siguiente manera: method update_actual_s(v :array<T>, i n i :int , old_s :i n t , new_k :int) returns (new_s :int) r e q u i r e s 0≤ini ≤old_s < new_k ≤v. Length r e q u i r e s s o r t e d ( v [ . . ] ) r e q u i r e s old_s =seg_long_max ( v [ . . ] , i n i , new_k −1 ).1 ensures 0≤new_s ≤new_k ensures new_s =seg_long_max ( v [ . . ] , i n i , new_k ) . 1 { new_s := old_s ; update_s_limits ( v [ . . ] , old_s , new_k ) ; var cond := m_true_on_segment ( v , new_s , new_k ) ; while(¬cond) decreases new_k −new_s invariant new_s ≤update_s ( v [ . . ] , old_s , new_k) invariant cond =is_true_on_segment ( v [ . . ] , new_s , new_k) { update_s_good_segment ( v [ . . ] , old_s , new_k ) ; new_s := new_s + 1 ; cond := m_true_on_segment ( v , new_s , new_k ) ; } update_s_min_value ( v [ . . ] , i n i , new_k ) ; update_s_is_seg_long_1 ( v [ . . ] , i n i , new_k −1); a s s e r t is_true_on_segment ( v [ . . ] , new_s , new_k ) ; update_s_if_snd ( v [ . . ] , i n i , old_s , new_k ) ; } El método principal es exactamente el mismo que el que se presentó en la subsección sobre propiedades cerradas por la izquierda, por lo que no se muestra. Se deja al usuario que demuestre para la propiedad que está estudiando los lemas siguientes, que se utilizan en la demostración del resto de lemas definidos en secciones anteriores. En primer lugar, se define de nuevo el lema closed_on_left_lemma(s : seq<T>) de una manera ligeramente diferente a como lo habíamos presentado antes. Ahora el vector estudiado lo pasamos como parámetro y además se le va a pedir al vector que esté ordenado. El predicado que ha de cumplir es el mismo que en casos anteriores. Así pues: 4.3. Abstracción y concreción sobre los problemas 41 lemma closed_on_left_lemma(s :seq<T>) r e q u i r e s s o r t e d ( s ) ensures ∀i n i , f i n , p | 0 ≤ini ≤p≤f i n ≤|s| ∧is_true_on_segment ( s , i n i , f i n ) •is_true_on_segment ( s , i n i , p ) En segundo lugar, se define un lema para expresar que la propiedad es cierta para el segmento vacío, que en nuestro caso viene representado por los segmentos cuyo inicio y fin son el mismo. De esta forma, el lema prop_is_true_on_void(v : seq<T>) queda definido de la siguiente manera: lemma prop_is_true_on_void(v :seq<T>) ensures ∀p | 0 ≤p≤|v| •is_true_on_segment(v , p, p) 4.3.5. Ejemplo El ejemplo elegido se ha extraído de los Apuntes de la asignatura de Estructuras de datos y algoritmos [12], y el algoritmo de resolución es el mismo para el problema de Acepta el reto sobre El hombre de seis dedos [10]. La implementación del código que se muestra a continuación la podemos encontrar en el módulo TestClosedLeftSorted en el archivo /seg_long_max/closed_left_sorted/test.dfy. El problema que vamos a estudiar es el siguiente: Problema. Dada un vector de enteros ordenado, queremos saber la longitud del segmento más largo que cumple que la diferencia entre todos sus elementos es menor que una cierta cantidad fija. La especificación del método que queremos obtener es la siguiente: {1≤n∧k≥1∧sorted(v)} method seg-long-max(v[0...n))return r : int {r= (max p, q : 0 ≤p≤q≤length(v)∧(v[q]−v[p]< k):(q−p)} Los extractos de código que se van a mostrar a continuación pueden encontrarse en el fichero /seg_long_max/closed_left_sorted/test.dfy del proyecto. Lo primero que debemos fijarnos es que este problema es uno de los tipos que hemos presentado, es un problema cuya propiedad es cerrada por la izquierda y que que es cierta para segmentos vacíos. Sabiendo esto, debemos crear un muevo módulo no abstracto que va a refinar a nuestro módulo SegLongMaxClosedLeftSorted. Lo primero que debemos hacer es fijar el parámetro k. Una vez hecho hecho esto, debemos definir la función is_true_on_segment y el método m_true_on_segment, acorde a nuestra propiedad. Esto aparece reflejado en el Figura 4.5 Ahora debemos demostrar los lemas closed_on_left_lemma yprop_is_true_on_void que hemos definido en el módulo abstracto. En este caso Dafny es capaz de verificarlo sin ayuda. Este proceso aparece reflejado en la Figura 4.6 Finalmente, creamos un método que llamará a nuestro método principal y utilizará nuestras postcondiciones para demostrar unas postcondiciones equivalentes que 42 Capítulo 4. Problemas de segmentos de longitud máxima const k :int := 4 ghost f u n c t i o n is_true_on_segment(v :seq<T>, i n i :int , f i n :int):(bool ) { i f ( i n i =f i n ) then t ru e e l s e v [ f i n −1] −v [ i n i ] < k } method m_true_on_segment(v :array<T>, i n i :i n t , f i n :int) returns ( r e s :bool ) { r e s := true ; i f ( i n i =f i n ) { r e s := v [ f i n −1] −v [ i n i ] < k ; } } Figura 4.5: Especifiación e implementación de la diferencia acotada lemma closed_on_left_lemma(s :seq<T>) {} lemma prop_is_true_on_void(v :seq<T>) ensures ∀p | 0 ≤p≤|v| •is_true_on_segment(v , p, p) {} Figura 4.6: Lemas para el problema de las diferencias acotadas hacen explícita las propiedades que cumple nuestro r. Este método es el que aparece en la Figura 4.7. 4.3. Abstracción y concreción sobre los problemas 43 method mseg_long_max_zero ( a :array<int >) returns ( r :int) r e q u i r e s s o r t e d ( a [ . . ] ) r e q u i r e s ∃p , q | 0 ≤p≤q≤| a [ . . ] | ∧( a [ q −1 ] −a [ p ] < k ) •q−p > 1 ensures ∀p , q | 0 ≤p≤q≤| a [ . . ] | ∧( a [ q −1 ] −a [ p ] < k ) •q−p≤r ensures ∃p , q | 0 ≤p≤q≤| a [ . . ] | ∧( a [ q −1 ] −a [ p ] < k ) •q−p=r { r:= mseg_long_max(a ); } Figura 4.7: Método principal de las diferencias acotadas Cap´ ıtulo 5 Problemas de contar segmentos En este capítulo se profundizará en el estudio de la verificación de los problemas de conteo de segmentos que cumplen una cierta propiedad. Los archivos que se corresponden con este capítulo se encuentran en las carpetas /cont_seg y/sliding_window. A la hora de afrontar la verificación de este tipo de problemas, se han tratado de manera muy similar a los de segmento de longitud máxima, aunque en este caso no se ha podido profundizar tanto, por lo que no se ha podido realizar una clasificación de los problemas tan exhaustiva. La estructura de este capítulo es, por tanto, muy similar a la del anterior. Se comienza explicando la abstracción realizada sobre este tipo de problemas, se presenta un tipo de problemas para los que podemos obtener una solución más eficiente y se ilustra con un ejemplo concreto. También se dedicará una sección al tipo de problemas llamados de “ventana deslizante”, que son un subtipo de estos problemas. 5.1. Modelado del problema El modelado del problema se encuentra contenido en el módulo ContSeg, que a su vez se encuentra en el fichero /cont_seg/cont_seg.dfy. Este módulo es el que a la hora de instanciar problemas concretos el usuario deberá refinar, y adaptarlo a la propiedad concreta estudiada. Comenzamos especificando el tipo de problemas que vamos a estudiar. Partimos de un vector vde nelementos y queremos devolver un rentero igual al número de segmentos no vacíos del vector tales que cumplen una cierta propiedad sobre segmentos A. Podemos escribir: Precondición :{n≥0} method cont-seg(v[0...n))return r : int Postcondición :{r= (# p, q : 0 ≤p<q≤n:A(v, p, q)} Para modelar la propiedad A, se ha utilizado la misma función is_true_on_segment que en el capítulo anterior. 45 52 Capítulo 5. Problemas de contar segmentos lemma valid_segments_fixed_last_count(v :seq<T>, i n i :i n t , f i n :int) decreases f i n −ini r e q u i r e s 0≤ini ≤f i n ≤|v| ensures ( f i n −min_pos_val ( v , i n i , f i n ) ) =| valid_segments_fixed_last(v, ini , fin )| Figura 5.2: Lema valid_segments_fixed_last_count de contar segmentos. lemma valid_segments_second(v :seq<T>, i n i :i n t , f i n :int) r e q u i r e s 0≤ini ≤f i n < | v | ensures ∀p , q | ( p , q ) i n valid_segm ents ( v , i n i , f i n ) •q≤f i n El último lema que definimos es valid_segments_void_intersection(v : seq<T>, fin : int) que nos asegura que la intersección entre los conjuntos que se muestran es vacía. Esta propiedad es necesaria para razonar sobre el cardinal de la unión, ya que el cardinal se actualiza sumando la cantidad de segmentos que cumplen la propiedad que no contemplábamos en el caso en que el extremo derecho era fin. Podemos proceder de esta forma porque los nuevos segmentos, al contener al elemento v[fin], no presentan elementos comunes con los ya calculados. lemma valid_segments_void_intersection(v :seq<T>, f i n :int) r e q u i r e s 0≤f i n < | v | ensures valid_segments ( v , 0 , f i n ) ∗valid_segments_fixed_last(v, 0, fin + 1) ={} Finalmente, queda por decir que todos los lemas que se han definido en este módulo, y aquellos que quedaban por demostrar en el módulo superior, han sido verificado por Dafny, con las indicaciones pertinentes para ello. 5.3. Ejemplo El ejemplo que se presenta a continuación está implementado en el módulo TestContSeg del archivo /cont_seg/test.dfy de nuestro proyecto. Para terminar de hablar de este tipo de problemas de contar segmentos, vamos a ver cómo se podría utilizar el modelo definido para trabajar con una propiedad concreta. El problema que hemos elegido es el siguiente: {n≥0} method cont-seg(v[0...N))return r : int {r= (# p, q : 0 ≤p<q≤n∧(∀k:p≤k < q :v[k] == 0} Es decir, estamos estudiando el número de segmentos dentro del vector vtales que todos sus elementos son 0. Para modelar este problema respecto a nuestro modelo, lo primero que debemos hacer crear un nuevo módulo que implemente nuestro ejemplo y que refine alguno de los módulos abstractos que hemos definido en la sección anterior. 5.4. Problemas de ventana deslizante 53 Como nuestra propiedad es del tipo estudiado en la última sección, refinamos el módulo ContSegForAllP. Como vamos a trabajar con vectores de enteros, fijamos el tipo abstracto Tal tipo de los enteros. Lo siguiente que debemos hacer es implementar la función que modela el predicado Py el método correspondiente: type T = int ghost f u n c t i o n is_true_on_elem(elem :T) :bool { elem =0 } method m_is_true_elem ( elem :T) returns ( r e s :bool ) { r e s := elem =0 ; } Finalmente, creamos un método que va a llamar al método principal de nuestro módulo abstracto. Hemos querido mostrar la postcondición de manera explícita para así poder entender mejor el problema que estamos resolviendo: method m_all_zero(v :array<in t >, l :int)returns ( r :int) r e q u i r e s 1≤l≤v. Length ensures r=|set p , q | 0 ≤p < q ≤v. Length ∧(∀k | p ≤k < q •v [ k ] =0) •(p , q ) | { r:= mcount_seg ( v ) ; valid_segments_snd ( v [ . . ] , 0 , v . Length ) ; } 5.4. Problemas de ventana deslizante Para terminar este capítulo se presenta un tipo de problemas de contar segmentos en el que la longitud del vector está fijada por un parámetro adicional que se añade al método principal. El modelado de este tipo de problemas en Dafny se presenta en la carpeta /sliding_window del proyecto. La filosofía que se va a seguir a la hora de presentar estos problemas es la misma que se ha seguido en anteriores secciones, pero en este caso de manera más resumida, ya que se han reutilizado muchas definiciones de los problemas de contar segmentos. 5.4.1. Modelado del problema Comenzamos presentando la especificación del problema, que es muy similar a la de contar segmentos: Precondición :{n≥0∧l≥1} method sliding-window(v[0...n), l : entero)return r : int Postcondición :{r= (# p: 0 ≤p−l < p ≤n∧A(v, p −l, p)} 54 Capítulo 5. Problemas de contar segmentos Las funciones is_true_on_segment,we_counted_rigth,valid_segments_fixed_last y valid_segments realizan el mismo cometido que en los problemas de contar segmentos, por lo que no se van a volver a explicar. La diferencia principal es que ahora incorporamos el parámetro l, que nos va a permitir simplificar muchos métodos y funciones, ya que tenemos que contemplar muchos menos casos. Las funciones quedan entonces definidas de la siguiente manera: ghost f u n c t i o n we_counted_rigth(v :seq<T>, r :i n t , l :int):bool r e q u i r e s l≥1 { r=| valid_segments (v , 0 , | v | , l ) | } ghost f u n c t i o n valid_segments_fixed_last(v :seq<T>, i n i :i n t , f i n :int , l :int) :set <(int ,int)> r e q u i r e s 0≤ini ≤f i n ≤|v| r e q u i r e s l≥1 { i f ( f i n −l≥ini ∧is_true_on_segment(v , fin −l , f i n )) then {( f i n −l , f i n )} else {} } ghost f u n c t i o n valid_segments(v :seq<T>, i n i :i n t , f i n :int , l :int) :set <(int ,int)> r e q u i r e s 0≤ini ≤f i n ≤|v| r e q u i r e s l≥1 { i f ( i n i =f i n ) then {} else valid_segm ents ( v , i n i , f i n −1 , l ) + valid_segments_fixed_last(v , ini , fin , l ) } La función min_pos_val se mantiene igual, ya que aunque a la hora de considerar nuevos segmentos solo podemos contemplar uno de ellos, el [fin - l, fin), nos servirá para comprobar en tiempo constante si debemos considerar el segmento actual para incrementar r. Igual ocurre con los métodos y el lema definidos en la sección anterior, realizan la misma función pero ahora incluyen un nuevo parámetro ly la precondición de que lsea mayor o igual que uno, ya que el caso vacío no se contempla. Los métodos y el lema quedan por tanto definidos de la siguiente manera como se observa en la Figura 5.3 Una vez modelado este tipo de problemas, podemos pasar a estudiar un subtipo concreto de estos, y así poder finalizar la implementación de todas las definiciones que quedan pendientes en el módulo abstracto, exceptuando aquella que depende de la propiedad concreta. 5.4.2. Propiedades universales sobre elementos En esta sección presentamos los problemas similares a los estudiados en las secciones homólogas de los otros tipo de problemas, pero ahora adaptando nuestras soluciones a las características concretas de nuestro problema. El modelado en Dafny explicada en esta subsección, se encuentra en el módulo SlidingWindowForAllP en el 5.4. Problemas de ventana deslizante 55 method variable_initialization(v :array<T>, l :int) returns ( r :int , k :i n t , n :int) r e q u i r e s 1≤l≤v. Length ensures 0≤k≤n≤v. Length ensures r=| valid_segments ( v [ . . ] , 0 , n , l ) | ensures k=min_pos_val ( v [ . . ] , 0 , n) method update_seg_count ( v :array<T>, r :i n t , old_limit :int , k :i n t , l :int) returns (new_r :int) r e q u i r e s 0≤o l d _ l i m i t < v . Length r e q u i r e s l≥1 r e q u i r e s k=min_pos_val ( v [ . . ] , 0 , o l d _ l i m i t + 1) r e q u i r e s r=| valid_segments ( v [ . . ] , 0 , o ld_limi t , l ) | ensures new_r =| valid _s eg me nt s ( v [ . . ] , 0 , o l d _ l i m i t + 1 , l ) | method update_lower_limit ( v :array<T>, i n i :int , old_lw :int , new_up :int) returns (new_lw :int) r e q u i r e s 0≤ini ≤old_lw < new_up ≤v. Length r e q u i r e s old_lw =min_pos_val ( v [ . . ] , i n i , new_up −1) ensures 0≤new_lw ≤new_up ensures new_lw =min_pos_val ( v [ . . ] , i n i , new_up) method mcount_seg ( v :array<T>, l :int) returns ( r :int) r e q u i r e s 1≤l≤v. Length ensures we_counted_rigth ( v [ . . ] , r , l ) lemma valid_segments_snd ( v :seq<T>, i n i :i n t , f i n :int , l :int) r e q u i r e s 0≤ini ≤f i n ≤|v| r e q u i r e s l≥1 ensures val id _s eg ments ( v , i n i , f i n , l ) =set p | i n i ≤p−l < p ≤f i n ∧is_true_on_segment(v , p −l , p ) •( p −l , p ) Figura 5.3: Principales métodos y lemas para los problemas de ventana deslizante. fichero /sliding_window/unitary.pdf. El módulo en cuestión refina el módulo abstracto SlidingWindow por lo que las funciones y métodos son los mismos que los explicados en la anterior subsección. En este caso el invariante es el mismo que en el caso de contar segmentos, al tener el límite inferior fijo. Como en otras secciones, lo primero que definimos es una función is_true_on_elem que se refenciará en la implementación del is_true_on_segment. Quedan así definidos las funciones. Cada función viene acompañada de su respectivo método, para mantener la separación entre implementación y especificación. Si no mantuviésemos la variable ken el método principal, nos veríamos obligados a incluir también un método m_is_true_on_segment como el que se muestra en la Figura 5.4, lo que provocaría que el coste en tiempo de nuestro algoritmo fuese cuadrático. Este método sería necesario en caso de tener que comprobar la propiedad en todo el segmento, pero esto no ocurre para el tipo de propiedades al que nos estamos restringiendo. Ahora que hemos definido las funciones que van a regir nuestro modelo y algún método asociado, podemos pasar a implementar los métodos principales, que como ya se ha explicado, son los mismos que en el caso de contar segmentos. 56 Capítulo 5. Problemas de contar segmentos method m_is_true_on_segment(v :array<T>, i n i :i n t , f i n :int) returns ( r e s :bool ) r e q u i r e s 0≤ini ≤f i n ≤v . Length ensures r e s =is_true_on_segment ( v [ . . ] , i n i , f i n ) { var cond , aux , i := true ,true , i n i ; while i < f i n ∧cond invariant i≤f i n invariant cond =is_true_on_segment ( v [ . . ] , i n i , i ) { aux := m_is_true_elem ( v [ i ] ) ; cond := cond ∧aux ; i:= i + 1 ; } r e s := cond ; } Figura 5.4: Ejemplo de m_is_true_on_segment ineficiente. El primero de ellos es variable_initialization, en este caso pedimos como precondición que la longitud del vector sea mayor que l. Recorremos los primeros l elementos para comprobar si se cumple la propiedad para este primer segmento, debemos recorrerlo entero, pues también estamos calculando el valor k. El método queda implementado como aparece en la Figura 5.5. El método update_seg_count simplemente comprueba si el nuevo posible segmento, [n - l, n) cumple la propiedad, para ello comprueba si el límite inferior del segmento es mayor o igual que k, y actualiza el contador en consecuencia. La implementación del método se puede observar en la Figura 5.6. El método update_lower_limit es igual que su homólogo de contar segmentos, por lo que no lo presentamos. Finalmente presentamos el método principal, que sigue el mismo esquema que en casos anteriores: method mcount_seg ( v :array<T>, l :int)returns ( r :int) { var n:int , k :int ; r , k , n := variable_initialization(v, l ); while n < v . Length invariant 0≤k≤n≤v. Length invariant k=min_pos_val ( v [ . . ] , 0 , n) invariant r=| valid_segments ( v [ . . ] , 0 , n , l ) | { min_pos_val_snd ( v [ . . ] , 0 , n + 1 ) ; k:= update_lowe r_li mit ( v , 0 , k , n + 1 ) ; r:= update_seg_count ( v , r , n , k , l ) ; n:= n + 1 ; } } Para terminar la subsección, presentamos algunos lemas auxiliares que son de utilidad a la hora de llevar a cabo la verificación. Se presentan las definiciones en la Figura 5.7. Todos estos lemas han sido demostrados en el módulo descrito, así como 5.4. Problemas de ventana deslizante 57 method variable_initialization(v :array<T>, l :int) returns ( r :int , k :i n t , n :int) { n:= l ; valid_segments_shorter_than_l(v [..] , 0, n −1 , l ) ; r:= 0; k := 0 ; var cond , aux , i := true ,true , 0 ; while i < n invariant k≤i≤n invariant cond =is_true_on_segment ( v [ . . ] , 0 , i ) invariant k=min_pos_val ( v [ . . ] , 0 , i ) { aux := m_is_true_elem ( v [ i ] ) ; cond := cond ∧aux ; i f (¬aux ) { k := i + 1; } i:= i + 1 ; } i f ( cond ) { r := 1; } } Figura 5.5: Implementación de variable_initialization para ventana deslizante aquellos definidos y no demostrados en el módulo abstracto. 5.4.2.1. Ejemplo Como en módulos anteriores, presentamos un ejemplo del tipo de problemas que podemos resolver haciendo uso de este módulo. La implementación que se muestra puede encontrarse en el módulo TestSlidingWindow que se encuentra en el fichero code/sliding_window/test.dfy. Problema. Dado un vector, queremos conocer el número de segmentos de una longitud fija lque cumplen que todos sus elementos son pares. Se supone que el vector proporcionado tiene una longitud de, al menos, l. Como en otros casos, lo primero que tenemos que definir son la función is_true_on_elem y el método m_is_true_elem. También fijamos el tipo de los vectores con los que estamos trabajando. Se muestran en la Figura 5.8. Y ahora ya podemos implementar el siguiente método principal, que aparece en la Figura 5.9. 58 Capítulo 5. Problemas de contar segmentos method update_seg_count ( v :array<T>, r :i n t , old_limit :int , k :i n t , l :int) returns (new_r :int) { var new_limit := old_limit + 1; new_r := r ; min_pos_val_limits ( v [ . . ] , 0 , new_limit ) ; min_pos_val_snd ( v [ . . ] , 0 , new_limit ) ; no_need_to_come_back ( v [ . . ] , 0 , new_limit ) ; i f ( new_limit −l≥0){ var cond := k≤new_limit −l ; i f ( cond ) { new_r := r + 1 ; valid_segments_second ( v [ . . ] , 0 , old_limi t , l ) ; } } } Figura 5.6: Implementación de update_seg_count para ventana deslizante. lemma valid_segments_second(v :seq<T>, i n i :i n t , f i n :int , l :int) r e q u i r e s 0≤ini ≤f i n < | v | r e q u i r e s l≥1 ensures ∀p , q | ( p , q ) i n vali d_ se gments ( v , i n i , f i n , l ) •q≤f i n lemma valid_segments_fixed_last_shorter_than_l ( v :seq<T>, i n i :i n t , f i n :i n t , l :int) r e q u i r e s 0≤ini ≤f i n ≤|v| r e q u i r e s l≥1∧( f i n −l ) < i n i ensures valid_segments_fixed_last(v, ini , fin , l ) ={} lemma valid_segments_shorter_than_l ( v :seq<T>, i n i :i n t , f i n :i n t , l :int) r e q u i r e s 0≤ini ≤f i n ≤|v| r e q u i r e s l≥1∧( f i n −i n i ) < l ensures val id _s eg ments ( v , i n i , f i n , l ) ={} lemma valid_segments_snd ( v :seq<T>, i n i :i n t , f i n :int , l :int) lemma min_pos_val_limits ( v :seq<T>, i n i :int , f i n :int) r e q u i r e s 0≤ini ≤f i n ≤|v| ensures ini ≤min_pos_val ( v , i n i , f i n ) ≤f i n lemma min_pos_val_snd ( v :seq<T>, i n i :in t , f i n :int) r e q u i r e s 0≤ini ≤f i n ≤|v| r e q u i r e s ini ≤min_pos_val ( v , i n i , f i n ) ≤f i n ensures is_true_on_segment ( v , min_pos_val ( v , i n i , f i n ) , f i n ) lemma closed_on_left_lemma() ensures ∀i n i , f i n , p , s :seq<T> | 0 ≤ini ≤p≤f i n ≤|s| ∧ is_true_on_segment ( s , i n i , f i n ) •is_true_on_segment ( s , i n i , p ) lemma no_need_to_come_back ( s :seq<T>, i n i :int , f i n :int) r e q u i r e s 0≤ini ≤f i n ≤|s| ensures ∀p:int | i n i ≤p < min_pos_val ( s , i n i , f i n ) ≤f i n • ¬is_true_on_segment ( s , p , f i n ) Figura 5.7: Lemas para propiedades universales en ventana deslizante 5.4. Problemas de ventana deslizante 59 type T = int ghost f u n c t i o n is_true_on_elem(elem :T) :bool { elem % 2 =0 } method m_is_true_elem ( elem :T) returns ( r e s :bool ) { r e s := elem % 2 =0; } Figura 5.8: Especificación e implementación de la propiedad en el ejemplo de ventana deslizante. method m_all_zero(v :array<in t >, l :int)returns ( r :int) r e q u i r e s 1≤l≤v. Length ensures r=|set p | 0 ≤p−l < p ≤v . Length ∧(∀k | p −l≤k < p •v [ k ] % 2 =0) •( p −l , p ) | { r:= mcount_seg ( v , l ) ; valid_segments_snd ( v [ . . ] , 0 , v . Length , l ) ; } Figura 5.9: Ejemplo de ventana deslizante donde todos son pares. Cap´ ıtulo 6 Conclusiones y Trabajo Futuro En este capítulo se tratará de resumir el trabajo llevado a cabo durante el desarrollo del proyecto, las conclusiones a las que se ha llegado con respecto a las metas propuestas al inicio, las dificultades encontradas y posible líneas de trabajo futuro. Con respecto a las metas que se propusieron al principio del proyecto, se ha llevado a cabo con éxito la resolución de bastantes de ellas, mientras que otras han quedado en el tintero. Se ha conseguido abstraer diferentes tipos de problemas sobre segmentos, y se han verificado utilizando la herramienta Dafny, pero en un inicio se propusieron más tipos de problemas que no se han podido llegar a abordar. Por lo tanto, una de las posibles líneas para continuar trabajando en este tema en un futuro sería precisamente tratar de abordar los tipos de problemas que no se han tratado, que son los mencionados en la Sección 3.4. Otra de las posible líneas de investigación sería seguir estudiando los problemas de este trabajo. No hemos contemplado tratar por separado propiedades cuya propiedad fuera exclusivamente cerrada por la derecha, ya que se ha considerado que se llegaría a resultados similares. Tampoco se ha profundizado como un caso aparte en el caso de propiedades que son disyunciones de otras propiedades más simples. Un ejemplo de este tipo de problemas sería la propiedad que comprueba si el producto de los elementos del segmento es positiva, para resolverlo de manera iterativa debemos tener en cuenta dos propiedades, que el número de positivos y el número de negativos del segmento en curso. Este ejemplo aparece en el problema 23 del Capítulo 4del libro Algoritmos correctos y eficientes [11]. Para finalizar, voy a describir las dificultades que he encontrado y los conocimientos que he adquirido. La verificación formal de programas es un campo al que me sentía atraído antes de comenzar este trabajo, y es por eso que elegí este tema para mi proyecto de fin de carrera. Cabe decir que antes de este trabajo nunca había tenido que enfrentarme a esta forma de crear código, ya que asignaturas anteriores (como Fundamentos de Algoritmia) se me había animado a plantear los problemas siguiendo la fórmula de precondición-postcondición, pero nunca había tratado de demostrar la corrección de mis algoritmos. 61