Especificación de algoritmos PDF

2.- Especificación de algoritmos Ignacio Fábregas - [email protected] Fundamentos de Algoritmia (FAL) Grupos E y F Grado en Ingeniería del Software...

2.- Especificación de algoritmos Ignacio Fábregas - [email protected] Fundamentos de Algoritmia (FAL) Grupos E y F Grado en Ingeniería del Software Fac. Informática (Transparencias basadas en originales de Clara Segura) Ignacio Fábregas - [email protected] 2.- Especificación de algoritmos Fac. Informática - UCM 1 / 38 Contenidos 1 Programación en la vida real 2 Especificación Vs. implementación 3 Especificación pre/post Lógica de primer orden 4 Especificación de funciones 5 Resumen Ignacio Fábregas - [email protected] 2.- Especificación de algoritmos Fac. Informática - UCM 2 / 38  Programación en la vida real Ignacio Fábregas - [email protected] 2.- Especificación de algoritmos Fac. Informática - UCM 3 / 38 Ignacio Fábregas - [email protected] 2.- Especificación de algoritmos Fac. Informática - UCM 4 / 38  Especificación Vs. implementación Ignacio Fábregas - [email protected] 2.- Especificación de algoritmos Fac. Informática - UCM 5 / 38 Algoritmo Definición Un algoritmo es la descripción abstracta y precisa de una sucesión de instrucciones que permiten llevar a cabo un trabajo en un número finito de pasos. Programa Un programa es la codificación en un lenguaje de programación concreto de un algoritmo. A la hora de desarrollar un algoritmo, seguimos los siguientes pasos: 1. Describir (especificar) el problema a resolver. 2. Programar (implementar) el método descrito anteriormente. Ignacio Fábregas - [email protected] 2.- Especificación de algoritmos Fac. Informática - UCM 6 / 38 Especificación e implementación Especificar Consiste en detallar cuidadosamente el problema que se quiere resolver. Contesta a la pregunta ¿Qué hace el algoritmo?, sin dar ningún detalle de cómo se hace. Una especificación debe ser tanto clara como precisa. La especificación debe responder a cualquier pregunta sobre el uso del algoritmo sin tener que acudir a la implementación. Implementar Consiste en decir cómo se resuelve el problema. Es programar el algoritmo en un lenguaje concreto (el nuestro es C++). Ignacio Fábregas - [email protected] 2.- Especificación de algoritmos Fac. Informática - UCM 7 / 38 Especificación como contrato: ingeniería del software La especificación de un algoritmo tiene un doble destinatario: Usuarios del algoritmo: ha de detallar las obligaciones del usuario al invocarlo y el resultado producido si es invocado correctamente. Restringe los datos de entrada. Implementador del algoritmo: define los requisitos que cualquier implementación válida debe satisfacer. Son los requisitos a satisfacer por todo programa válido. La especificación permite independizar los razonamientos de corrección de cada componente: Ignacio Fábregas - [email protected] 2.- Especificación de algoritmos Fac. Informática - UCM 8 / 38 Propiedades de una especificación 1. Precisión: debe evitar malentendidos y ambigüedades. El lenguaje natural no permite la precisión necesaria (salvo si se sacrifica la brevedad). 2. Brevedad: ha de ser significativamente más breve que el código al que especifica. Los lenguajes formales ofrecen a la vez precisión y brevedad. 3. Claridad: ha de transmitir la intuición de lo que se pretende. Exige conocimiento y experiencia en algún lenguaje formal. A veces hay que complementar con explicaciones informales. Ignacio Fábregas - [email protected] 2.- Especificación de algoritmos Fac. Informática - UCM 9 / 38 Especificación formal: uso de lógica Elimina posibles ambigüedades. Se evitan interpretaciones dispares entre el usuario y el implementador. Permite realizar verificación formal del algoritmo. Razonar la corrección del algoritmo desde la lógica. También permite derivar la implementación desde una especificación (verás detalles de esto en el siguiente tema). Permite generar automáticamente casos de prueba. Uso de testing, una técnica que permite generar casos de prueba que garanticen que nuestro programa es correcto. Ignacio Fábregas - [email protected] 2.- Especificación de algoritmos Fac. Informática - UCM 10 / 38  Especificación pre/post Ignacio Fábregas - [email protected] 2.- Especificación de algoritmos Fac. Informática - UCM 11 / 38 Ejemplo Queremos una función que, dados el vector vector v de tamaño 1000 y un entero n, devuelva un booleano b que indique si el valor de alguno de los elementos v,... v[n-1] es igual a la suma de todos los elementos que le preceden en el vector: bool essuma ( const vector & v, int n) Podemos pensar que con la cabecera de C++ es suficiente: indica qué recibe y qué tipo devuelve. ¿Te quedan claro todas las obligaciones del usuario? ¿Es decir, sabes qué va a ocurrir si usases esta función de una librería? ¿Puede ser n negativo? ¿n = 0 es válido? ¿Pasaría algo si n ≥ 1000? Tampoco están claras las obligaciones del implementador, es decir, ¿si te toca implementar esta función, sabes qué debería devolver?: ¿Si v= 0 se devuelve true o false? Ignacio Fábregas - [email protected] 2.- Especificación de algoritmos Fac. Informática - UCM 12 / 38 Cabecera de una función Normalmente se usan lenguajes diferentes para describir la implementación (el código) de la especificación. Si bien nosotros usaremos lógica de primer orden para describir la especificación, usaremos la notación de C++ para describir la cabecera de la función. essuma bool essuma ( const vector & v, const int n) Las variables de entrada se indican con la palabra reservada const. La(s) variable(s) que se devuelven mediante return, se indican con un comentario. En este caso la función sólo devuelve una variable bool que será la variable b. Las variables de salida se indican mediante el ampersand: &. Ignacio Fábregas - [email protected] 2.- Especificación de algoritmos Fac. Informática - UCM 13 / 38 Cabecera de una función: observación En C++, las variables de tipo básico (bool, int, float, etc) se pasan, por defecto, por copia. No es necesario indicar que una variable entera es constante, por lo tanto. Lo indicaremos para hacer explícito que, en la especificación, esta variable es de entrada. En C++, las variables de tipo compuesto (string, vector, etc) se deben pasar por referencia para evitar copias innecesarias. Siempre las pasaremos usando el ampersand &. Indicamos que es de entrada usando, como antes, la palabra reservada const. Ignacio Fábregas - [email protected] 2.- Especificación de algoritmos Fac. Informática - UCM 14 / 38 Especificación formal Como decíamos, para escribir especificaciones sin ambigüedades y precisas, necesitamos un lenguaje forma. La especificación pre/post (C.A.R. Hoare, 1969) contempla al programa A como una caja negra. A actúa como una función de estados en estados: Comienza la ejecución en un estado descrito por los valores de los parámetros de entrada. Ejecuta las instrucciones de la función/programa. Termina en un estado final en el que los parámetros de salida contienen los resultados esperados. Se denota {P} A {Q} para indicar los valores iniciales de las variables de entrada ({P}) y los valores de salida ({Q}). Ignacio Fábregas - [email protected] 2.- Especificación de algoritmos Fac. Informática - UCM 15 / 38 Volviendo al ejemplo Especificación {0 ≤ n ≤ 1000} bool essuma(const vector& v, const int n) ∑ {b = ∃i, 0 ≤ i < n, v[i] = 0≤j 0 y v= 0, la función debe devolver b =true. Ignacio Fábregas - [email protected] 2.- Especificación de algoritmos Fac. Informática - UCM 16 / 38 {P} S {Q} formalmente Precondición P se llama precondición. Caracteriza el conjunto de estados iniciales para los que está garantizado que el algoritmo funciona correctamente. Describe las obligaciones del usuario: si se llama al algoritmo en un estado que no satisface P, no es posible afirmar lo que sucederá. Postcondición Q se llama postcondición. Caracteriza la relación entre cada estado inicial, supuesto válido, y el estado final correspondiente. Describe las obligaciones del implementador, que debe garantizar que el algoritmo termina en un estado que satisfaga Q. Ignacio Fábregas - [email protected] 2.- Especificación de algoritmos Fac. Informática - UCM 17 / 38  Lógica de primer orden Ignacio Fábregas - [email protected] 2.- Especificación de algoritmos Fac. Informática - UCM 18 / 38 Sintaxis de la lógica de primer orden Una fórmula de primer orden, o un predicado es: una fórmula atómica: las constantes true y false. variables booleanas b. expresiones aritméticas relacionales como x = y o n < 0. funciones matemáticas que devuelvan booleanos. Si P es un predicado, ¬P, leído “no P”, también lo es. Si P y Q son predicados, P & Q también lo es, siendo & cualquiera de las conectivas lógicas {∧, ∨, →, ↔}, leídas respectivamente “y”, “o”, “entonces”, “si y solo si”. Si P y Q son predicados, (∀w : Q(w) : P(w)) y (∃w : Q(w) : P(w)) también lo son, denominados respectivamente cuantificación universal y cuantificación existencial. Ignacio Fábregas - [email protected] 2.- Especificación de algoritmos Fac. Informática - UCM 19 / 38 Ejemplos de predicados: sintaxis n≥0 x > 0 ∧ x 6= y 0≤i 0 cuenta el número de elementos positivos del vector (v[i] > 0), entre las posiciones a y b. Ignacio Fábregas - [email protected] 2.- Especificación de algoritmos Fac. Informática - UCM 22 / 38 Ejemplo: moda de un vector La moda de un vector es el elemento que más veces aparece en un vector. Consideramos v de tamaño n. Primero vamos a expresar la frecuencia de un elemento, es decir, el número de veces que aparece un elemento. Esto se conoce como predicado auxiliar: frec(v, e) = # i : 0 ≤ i < n : v[i] = e. La moda es el máximo de las frecuencias, es decir, moda(v) = máx i : 0 ≤ i < n : frec(v, v[i]) Observa que aunque en principio podría haber infinitos valores e para los que contar la frecuencia, en realidad, sólo nos importan los valores que ya están presentes en el vector. De ahí que llamemos con los valores v[i]. Ignacio Fábregas - [email protected] 2.- Especificación de algoritmos Fac. Informática - UCM 23 / 38 Tipos de variables en un predicado Variables ligadas: Están dentro del ámbito de un cuantificador. ∑ ∏ ∀ y ∃, pero también , , máx, mı́n y #. Variables libres: No se encuentran afectadas por ningún cuantificador. Son las variables del programa. Una variable ligada se puede renombrar sin cambiar el significado del predicado. (∃w : 0 ≤ w < n : a[w] = x) ≡ (∃j : 0 ≤ j < n : a[j] = x) Hay que utilizar identificadores diferentes en las variables ligadas para evitar errores. Hay que utilizar identificadores diferentes para las variables libres de los usados en las variables ligadas. Ignacio Fábregas - [email protected] 2.- Especificación de algoritmos Fac. Informática - UCM 24 / 38 Semántica: teoría Utilizaremos predicados para definir conjuntos de estados. Estado Asociación de las variables del algoritmo con valores compatibles con su tipo. Un estado σ satisface un predicado P si al sustituir en P las variables libres por los valores que esas variables tienen en σ el predicado evalúa a cierto. Por ejemplo, σ = {x 7→ 5, y 7→ 0} representa un estado en la que la variable x vale 5 y la y 0. σ satisface el predicado P ≡ x − y > 0 pero no el predicado Q ≡ x ∗ y > 0. Identificaremos un predicado con el conjunto de estados que lo satisfacen. Ese conjunto puede ser vacío o infinito. Ignacio Fábregas - [email protected] 2.- Especificación de algoritmos Fac. Informática - UCM 25 / 38 Semántica: práctica El predicado true indica que las variables pueden tomar cualquier valor. Siempre se cumple. El predicado false no se cumple para ningún valor de las variables. Define el conjunto vacío. Por lo tanto, no tiene sentido su uso en la precondición. En la postcondición indica que el programa no termina. ∀i : Q(i) : P(i) se corresponde con P(i1 ) ∧ P(i2 ) ∧..., donde i1 , i2 ,... son todos los valores de i que hacen cierto Q(i). ∀ únicamente es falso si hay un caso en el que no se cumple la condición. ∀i : 0 ≤ i < n : v[i] > 0 es falso si existe un índice a entre [0, n) tal que v[a] ≤ 0. Si el conjunto Q es vacío, por ejemplo arriba n = 0, el predicado es equivalente a true. Ignacio Fábregas - [email protected] 2.- Especificación de algoritmos Fac. Informática - UCM 26 / 38 Semántica: práctica ∃i : Q(i) : P(i) se corresponde con P(i1 ) ∨ P(i2 ) ∨..., donde i1 , i2 ,... son todos los valores de i que hacen cierto Q(i). ∃ únicamente es cierto si hay un caso en el que se cumple la condición. ∃i : 0 ≤ i < n : v[i] > 0 es cierto si hay un índice a entre [0, n) tal que v[a] > 0. ∃i : 0 ≤ i < n : v[i] > 0 es falso si hay para todos los índices a entre [0, n), v[a] ≤ 0. Si el conjunto Q es vacío, por ejemplo arriba n = 0, el predicado es equivalente a false. Ignacio Fábregas - [email protected] 2.- Especificación de algoritmos Fac. Informática - UCM 27 / 38 Semántica: práctica Existen valores por definición cuando el rango Q(i) al que pertenece la variable i cuantificada es vacío: ∑ ( i : false : e(i)) = 0 ∏ ( i : false : e(i)) = 1 (máx i : false : e(i)) indefinido (mı́n i : false : e(i)) indefinido (# i : false : P(i)) = 0 Ignacio Fábregas - [email protected] 2.- Especificación de algoritmos Fac. Informática - UCM 28 / 38 Semántica: Predicado más débil y más fuerte Como tantas cosas de este tema, esto tendrá más utilidad en el siguiente tema (para poder escribir mejores precondiciones y postcondiciones). P es un predicado más fuerte que Q, P ⇒ Q, si el conjunto de estados que satisfacen P es un subconjunto del de estados que satisfacen Q: P ⊆ Q. (x > 3) ⇒ (x ≥ 0). Es más fuerte (es más concreto, más restrictivo) decir que una variable es mayor que 3, a decir que únicamente es mayor o igual a 0. P es un predicado más débil que Q, P ⇐ Q, si el conjunto de estados que satisfacen P es un superconjunto del de estados que satisfacen Q: P ⊇ Q. P y Q son equivalentes, P ≡ Q, cuando P ⇒ Q y P ⇐ Q. Ignacio Fábregas - [email protected] 2.- Especificación de algoritmos Fac. Informática - UCM 29 / 38  Especificación de funciones Ignacio Fábregas - [email protected] 2.- Especificación de algoritmos Fac. Informática - UCM 30 / 38 Especificaciones Identificamos un algoritmo con una función en C++. Las funciones tienen el tipo del resultado devuelto. Si no devuelven ningún valor, se usa el tipo void. Los mecanismos de paso de parámetros distinguen entre paso por valor, paso por referencia y paso por referencia constante. A efectos de una especificación es más ilustrativa la siguiente distinción: entrada Su valor inicial es relevante para el algoritmo y éste no debe modificarlo. salida Su valor inicial es irrelevante para el algoritmo y éste debe almacenar algún valor en él. entrada/salida Su valor inicial es relevante para el algoritmo y además este puede modificarlo Recuerda que ya hemos visto cómo vamos a anotar las cabeceras de las funciones. Ignacio Fábregas - [email protected] 2.- Especificación de algoritmos Fac. Informática - UCM 31 / 38 Ejemplos Devolver un número primo mayor o igual que un cierto valor {n>1} int unPrimo(const int n) { p ≥ n ∧ (∀i : 1 < i < p : p mód i 6= 0) } ¿Sería correcto devolver p = 2? La postcondición no determina un único p. Podemos devolver cualquier primo mayor o igual que n. Ignacio Fábregas - [email protected] 2.- Especificación de algoritmos Fac. Informática - UCM 32 / 38 Ejemplos Devolver el menor número primo mayor o igual que un cierto valor {n>1} int menorPrimo(const int n) { p ≥ n ∧ primo(p) ∧ (∀q : q ≥ n ∧ primo(q) : p ≤ q) } donde primo(x) ≡ (∀i : 1 < i < x : x mód i 6= 0). El predicado auxiliar primo(x) hace la especificación modular y más legible. primo(x) es una propiedad y no sugiere que la comprobación haya de hacerse dividiendo por todos los números menores que x. Recuerda, la especificación NO habla de la implementación de la función. La postcondición puede ser más concisa: p = (mı́n q : q ≥ n ∧ primo(q) : q). Ignacio Fábregas - [email protected] 2.- Especificación de algoritmos Fac. Informática - UCM 33 / 38 Ejemplos Queremos especificar una función que modifique los valores de un vector. Debe cambiar cada valor negativo del vector por el valor 0. En general, usaremos N para expresar el tamaño del vector v.size(). Positivizar un vector. Primer intento {N≥0} void positivizar(vector& v) { ∀i : 0 ≤ i < N : v[i] < 0→v[i] = 0 } Pero hay un problema: ¡hemos conseguido una postcondición equivalente a false!. v[i] no puede ser a la vez menor que 0 e igual a 0. v en la postcondición se refiere a su valor después de ejecutarlo, queremos decir que su valor ha cambiado después de ejecutar la función. Ignacio Fábregas - [email protected] 2.- Especificación de algoritmos Fac. Informática - UCM 34 / 38 Ejemplos Para indicar que el vector cambiará de valores a la hora de ejecutar un vector, indicamos en su precondición qué valores iniciales tiene. Positivizar un vector. Segundo intento { N≥0∧v=V } void positivizar(vector& v) { ∀i : 0 ≤ i < N : V[i] < 0→v[i] = 0 } La condición v = V (en la precondición) sirve para dar un nombre al valor del vector v antes de ejecutar el procedimiento. Así podemos distinguir el valor del vector antes (V) como después (v). Pero con esto no basta, ¡un implementador malévolo podría modificar también el resto de valores! Ignacio Fábregas - [email protected] 2.- Especificación de algoritmos Fac. Informática - UCM 35 / 38 Ejemplos La solución es indicar también que el resto de valores del vector no han tenido ningún cambio. Positivizar un vector. Tercer intento { N≥0∧v=V } void positivizar(vector& v) { ∀i : 0 ≤ i < N : (V[i] < 0→v[i] = 0) ∧ (V[i] ≥ 0→v[i] = V[i]) } En general, es más complicado especificar una función que modifique los valores de un vector que aquellas funciones que únicamente devuelven un valor sobre un vector. Ignacio Fábregas - [email protected] 2.- Especificación de algoritmos Fac. Informática - UCM 36 / 38  Resumen Ignacio Fábregas - [email protected] 2.- Especificación de algoritmos Fac. Informática - UCM 37 / 38 Mínimos del tema Especificar nos permite decir cómo esperamos que funcione un programa. La especificación NO tiene que hablar de la implementación particular usada, únicamente su comportamiento. Suele ser preferible dividir predicados en subpredicados más sencillos. Recuerda la lógica de primer orden. Ignacio Fábregas - [email protected] 2.- Especificación de algoritmos Fac. Informática - UCM 38 / 38  Capítulo 2 Especificación de algoritmos1 Las matemáticas son el alfabeto con el cual Dios ha escrito el Universo. Galileo Galilei (1564-1642) Resumen: En este tema se enseña a distinguir entre especificar e implementar algo- ritmos, se repasa la lógica de predicados, y se establecen convenios y notaciones para especificar funciones y procedimientos utilizando dicha lógica. 1. Introducción ? Especificar un algoritmo consiste en contestar a la pregunta “qué hace el algoritmo”, sin dar detalles sobre cómo consigue dicho efecto. Una actitud correcta consiste en contemplar el algoritmo como una caja negra de la que solo podemos observar sus entradas y sus salidas. ? Implementar, por el contrario, consiste en contestar a este segundo aspecto, es decir “cómo se consigue la funcionalidad pretendida”, suponiendo que dicha funcionalidad está perfectamente clara en la especificación. ? Muchos programadores noveles tienen dificultades para distinguir entre ambas activi- dades, produciendo documentos donde se mezclan continuamente los dos conceptos. ? La especificación de un algoritmo tiene un doble destinatario: Los usuarios del algoritmo: debe recoger todo lo necesario para un uso correcto del mismo. En particular, ha de detallar las obligaciones del usuario al invocar dicho algoritmo y el resultado producido si es invocado correctamente. El implementador del algoritmo: define los requisitos que cualquier implemen- tación válida debe satisfacer, es decir, las obligaciones del implementador. Ha de dejar suficiente libertad para que este elija la implementación que estime más adecuada con los recursos disponibles. 1 Ricardo Peña es el autor principal de este tema. 15 16 Capítulo 2. Especificación de algoritmos ? Una vez establecida la especificación, los trabajos del usuario y del implementador pueden proseguir por separado. La especificación actúa pues como una barrera o contrato que permite independizar los razonamientos de corrección de los distintos componentes de un programa grande. Así, se descompone la tarea de razonar sobre el mismo en unidades manejables que corresponden a su estructura modular. ? Propiedades de una buena especificación: Precisión Ha de responder a cualquier pregunta sobre el uso del algoritmo sin tener que acudir a la implementación del mismo. El lenguaje natural no permite la precisión requerida si no es sacrificando la brevedad. Brevedad Ha de ser significativamente más breve que el código que especifica. Los lenguajes formales ofrecen a la vez precisión y brevedad. Claridad Ha de transmitir la intuición de lo que se pretende. A veces el lenguaje formal ha de ser complementado con explicaciones informales. ? En este capítulo se presenta una técnica de especificación formal de funciones y procedimientos basada en el uso de la lógica de predicados, también conocida como técnica pre/post. Más adelante se presentará otra técnica formal diferente, las llamadas especificaciones algebraicas, más apropiadas para especificar tipos de datos. ? Las ventajas de una especificación formal frente a una informal son bastantes: Eliminan ambigüedades que el usuario y el implementador podrían resolver de formas distintas, dando lugar a errores de uso o de implementación que aparecerían en ejecución. Son las únicas que permiten realizar una verificación formal del algoritmo. Este tema se tratará en los capítulos 3 y 4, y consiste en esencia en razonar sobre la corrección del algoritmo mediante el uso de la lógica. Permite generar automáticamente un conjunto de casos de prueba que permitirán probar la corrección de la implementación. La especificación formal se usa para predecir y comprobar el resultado esperado. ? Supongamos declarado en alguna parte el siguiente tipo de datos: typedef int vect ; (2.1) Queremos una función que, dado un vector a de tipo vect y un entero n, devuelva un valor booleano b que indique si el valor de alguno de los elementos a,... , a[n 1] es igual a la suma de todos los elementos que le preceden en el vector. Utilizaremos la siguiente cabecera sintáctica: fun essuma (vect a, int n) return (bool b) ? Esta especificación informal presenta algunas ambigüedades: No quedan claras todas las obligaciones del usuario: (1) ¿serían admisibles lla- madas con valores negativos de n?; (2) ¿y con n = 0?; (3) ¿y con n > 1000? En caso afirmativo, ¿cuál ha de ser el valor devuelto por la función? Fundamentos de Algoritmia 2. Predicados 17 Tampoco están claras las obligaciones del implementador. Por ejemplo, si n 1 y a = 0 la función, ¿ha de devolver true o false? Tratar de explicar en lenguaje natural todas estas situaciones llevaría a una especi- ficación más extensa que el propio código de la función essuma. ? La siguiente especificación formal contesta a estas preguntas: P ⌘ {0  n  1000} fun essuma (vect a, int n) returnPbool b Q ⌘ {b = 9w : 0  w < n : a[w] = ( u : 0  u < w : a[u])} No son correctas llamadas con valores negativos de n, ni con n > 1000; sí son correctas llamadas con n = 0 y en ese caso ha de devolver false; las llamadas con n 1 y a = 0 han de devolver b = true. Para saber por qué, seguir leyendo. ? La técnica pre/post, debida a C.A.R. Hoare (1969), se basa en considerar que un algoritmo es una función de estados en estados: comienza su ejecución en un estado inicial válido descrito por el valor de los parámetros de entrada y, tras un cierto tiempo cuya duración no es relevante a efectos de la especificación, termina en un estado final en el que los parámetros de salida contienen los resultados esperados. ? Si S representa la función a especificar, P es un predicado que tiene como varia- bles libres los parámetros de entrada de S, y Q es un predicado que tiene como variables libres los parámetros de entrada y de salida de S, la notación {P }S{Q} es la especificación formal de S y ha de leerse: “Si S comienza su ejecución en un estado descrito por P , S termina y lo hace en un estado descrito por Q”. ? P recibe el nombre de precondición y caracteriza el conjunto de estados iniciales para los que está garantizado que el algoritmo funciona correctamente. Describe las obligaciones del usuario. Si este llama al algoritmo en un estado no definido por P , no es posible afirmar qué sucederá. ? Q recibe el nombre de postcondición y caracteriza la relación entre cada estado inicial, supuesto este válido, y el estado final correspondiente. Describe las obliga- ciones del implementador, supuesto que el usuario ha cumplido las suyas. 2. Predicados ? Usaremos las letras mayúsculas P , Q, R,... , para denotar predicados de la lógica de primer orden. La sintaxis se define inductivamente mediante las siguientes reglas: 1. Una expresión e de tipo bool es un predicado. 2. Si P es un predicado, ¬P , leído “no P ”, también lo es. 3. Si P y Q son predicados, P & Q también lo es, siendo & cualquiera de las conectivas lógicas {^, _, !, $}, leídas respectivamente “y”, “o”, “entonces”, “si y solo si”. Facultad de Informática - UCM 18 Capítulo 2. Especificación de algoritmos 4. Si P y Q son predicados, (8w : Q(w) : P (w)) y (9w : Q(w) : P (w)) también lo son, denominados respectivamente cuantificación universal y cuantificación existencial. En lógica de primer orden, estas cuantificaciones se escriben con una sintaxis más simple (respectivamente 8w. R(w) y 9w. R(w), siendo R un predicado). La sintaxis edulcorada propuesta aquí se escribiría entonces 8w. (Q(w)!P (w)) y 9w. (Q(w) ^ P (w)) respectivamente. La hemos elegido porque facilitará la escritura de asertos sobre programas. ? Algunos ejemplos de predicados: n 0 x > 0 ^ x 6= y 0i 0, pero no Q ⌘ x mód 2 = 0. ? Dado un predicado P , queda determinado con precisión el conjunto de todos los es- tados que satisfacen P. Adoptaremos entonces el punto de vista de identificar un predicado con el conjunto de estados que lo satisfacen. Este conjunto frecuen- temente es infinito y a veces es vacío. ? Suponiendo que x e y sean las únicas variables del algoritmo, P ⌘ y x > 0 define los infinitos pares (x, y) en los que y es mayor que x (es decir el semiplano encima de la diagonal principal del plano), mientras que Q ⌘ x mód 2 = 0 define todos los pares (x, y) en los que x es un número par. ? En particular, el predicado true define el conjunto de todos los estados posibles (i.e. cualquier variable del algoritmo puede tener cualquier valor de su tipo), y el predicado false define el conjunto vacío. ? El significado del predicado 8w : Q(w) : P (w) es equivalente al de la conjunción P (w1 ) ^ P (w2 ) ^..., donde w1 , w2 ,... son todos los valores de w que hacen cierto Q(w). Si este conjunto es vacío, entonces 8w : Q(w) : P (w) ⌘ true. ? El significado del predicado 9w : Q(w) : P (w) es equivalente al de la disyunción P (w1 ) _ P (w2 ) _..., donde w1 , w2 ,... son todos los valores de w que hacen cierto Q(w). Si este conjunto es vacío, entonces 9w : Q(w) : P (w) ⌘ false. ? Hay predicados que se satisfacen en todos los estados (e.g. x > 0 _ x  0). Equivalen a true. Hay otros que no se satisfacen en ninguno (e.g. 9w : 0 < w < 1 : a[w] = 8). Equivalen a false. Facultad de Informática - UCM 20 Capítulo 2. Especificación de algoritmos ? Por definición, el significado del resto de los cuantificadores cuando el rango Q(w) al que se extiende la variable cuantificada es vacío, es el siguiente: P (Q w : false : e(w)) = 0 ( w : false : e(w)) = 1 (máx w : false : e(w)) indefinido (mı́n w : false : e(w)) indefinido (# w : false : P (w)) = 0 ? Diremos que un predicado P es más fuerte (resp. más débil) que otro Q, y lo expresaremos P ) Q (resp. P ( Q), cuando en términos de estados se cumpla P ✓ Q (resp. P ◆ Q), es decir, todo estado que satisface P también satisface Q (resp. todo estado que satisface Q también satisface P ). x>0 ) x 0 P ^Q ) P P ^Q ) Q P ) P _Q 8w : 0  w < 10 : a[w] 6= 0 ) a 6= 0 ? El predicado más fuerte posible es false pues, para cualquier predicado P , false ) P. Simétricamente, el predicado más débil posible es true: para cualquier predicado P , P ) true. ? La relación “ser más fuerte que” coincide con la noción lógica de deducción. Leeremos con frecuencia P ) Q como “de P se deduce Q”, o “P implica Q”. ? Si P ) Q y Q ) P , diremos que son igual de fuertes, o igual de débiles, o sim- plemente que son equivalentes, y lo expresaremos como P ⌘ Q. Dos predicados equivalentes definen el mismo conjunto de estados. 4. Ejemplos de especificación ? Identificaremos un algoritmo con la noción de función en C++. En este lenguaje, las funciones tienen un tipo que corresponde al del resultado devuelto. Si no devuelven ningún valor, se usa el tipo void. Los mecanismos de paso de parámetros distinguen entre paso por valor, paso por referencia y paso por referencia constante. En esencia especifican si los parámetros formales de la función llamada son disjuntos o son los mismos que los parámetros reales del llamante. Se trata de un aspecto más relacionado con la eficiencia que con el flujo de información. ? A efectos de especificación es más ilustrativo saber si los parámetros son de entrada Su valor inicial es relevante para el algoritmo y este no debe modificarlo. salida Su valor inicial es irrelevante para el algoritmo y este debe almacenar algún valor en él. entrada/salida Su valor inicial es relevante para el algoritmo, y además este puede modificarlo. Fundamentos de Algoritmia 4. Ejemplos de especificación 21 ? Por ello, usaremos en la especificación dos tipos de cabeceras virtuales que el programador habrá de traducir después a la cabecera de función C++ que le parezca más apropiada. fun nombre (tipo1 p1 ,... , tipon pn ) return tipo r proc nombre (cualif tipo1 p1 ,... , cualif tipon pn ) donde cualif será vacío si el parámetro es de entrada, out si es de salida, o inout si es de entrada/salida. Los parámetros de una cabecera fun se entienden siempre de entrada. ? La primera se usará para algoritmos que devuelvan un solo valor, y la segunda para los que no devuelvan nada, devuelvan más de un valor, o/y modifiquen sus parámetros. ? Especificar un algoritmo que calcule el cociente y el resto de la división de naturales. Primer intento: {a 0 ^ b > 0} proc divide (int a, int b, out int q, out int r) {a = q ⇥ b + r} ? El especificador ha de imaginar que el implementador es un ser malévolo que trata de satisfacer la especificación del modo más simple posible, respetando la “letra” pero no el “espíritu” de la especificación. El siguiente programa sería correcto: {q = 0; r = a; } El problema es que la postcondición es demasiado débil. ? Segundo intento: {a 0 ^ b > 0} proc divide (int a, int b, out int q, out int r) {a = q ⇥ b + r ^ 0  r < b} Por conocimientos elementales de matemáticas sabemos que solo existen dos números naturales que satisfacen lo que exigimos a q y r. ? El máximo de las primeras n posiciones de un vector: {n > 0 ^ longitud (a) n} fun maximo (int a[ ], int n) return int m {(8w : 0  w < n : m a[w]) ^ (9w : 0  w < n : m = a[w])} La precondición n > 0 es necesaria para asegurar que el rango del existencial no es vacío. Una postcondición false solo la satisfacen los algoritmos que no terminan. La segunda conjunción de la precondicion requiere que el vector parámetro real tenga una longitud de al menos n. Nótese que la segunda conjunción de la postcondición es necesaria. Si no, el implementador malévolo podría devolver un número muy grande pero no nece- sariamente en el vector. Una postcondición más sencilla sería. {m = máx w : 0  w < n : a[w]} Facultad de Informática - UCM 22 Capítulo 2. Especificación de algoritmos ? Devolver un número primo mayor o igual que un cierto valor: {n > 1} fun unPrimo (int n) return int p {p n ^ (8w : 1 < w < p : p mód w 6= 0)} ¿Sería correcto devolver p = 2? Nótese que la postcondición no determina un único p. El implementador tiene la libertad de devolver cualquier primo mayor o igual que n. ? Devolver el menor número primo mayor o igual que un cierto valor: {n > 1} fun menorPrimo (int n) return int p {p n ^ primo(p) ^ (8w : w n ^ primo(w) : p  w)} donde primo(x) ⌘ (8w : 1 < w < x : x mód w 6= 0) Obsérvese que el uso del predicado auxiliar primo(x) hace la especificación a la vez más modular y legible. Nótese que un predicado no es una implementación. Por tanto no le son apli- cables criterios de eficiencia: primo(x) es una propiedad y no sugiere que la comprobación haya de hacerse dividiendo por todos los números menores que x. La postcondición podría expresarse de un modo más conciso: p = (mı́n w : w n ^ primo(w) : w) sin que de nuevo esta especificación sugiera una forma de implementación. ? Especificar un procedimiento que positiviza un vector. Ello consiste en reemplazar los valores negativos por ceros. Primer intento: {n 0 ^ longitud (a) = n} proc positivizar (inout int a[ ], int n) {8w : 0  w < n : a[w] < 0!a[w] = 0} Lo que conseguimos es una postcondición equivalente a false. ? Añadimos a la precondición la condición a = A que nos sirve para poder dar un nombre al valor del vector a antes de ejecutar el procedimiento, ya que a en la postcondición se refiere a su valor después de ejecutarlo. Segundo intento: {n 0 ^ longitud (a) = n ^ a = A} proc positivizar (inout int a[ ], int n) {8w : 0  w < n : A[w] < 0!a[w] = 0} ? El implementador malévolo podría modificar también el resto de valores. Tercer in- tento: {n 0 ^ longitud (a) = n ^ a = A} proc positivizar (inout int a[ ], int n) {8w : 0  w < n : (A[w] < 0!a[w] = 0) ^ (A[w] 0!a[w] = A[w])} Fundamentos de Algoritmia Notas bibliográficas 23 Notas bibliográficas Se recomienda ampliar el contenido de estas notas estudiando el Capítulo 2 de (Peña, 2005) en el cual se han basado, si bien la notación para predicados es ligeramente diferente. También la Sección 1.1 de (Rodríguez Artalejo et al., 2011). El Capítulo 1 de Martí Oliet et al. (2012) utiliza la misma notación de predicados empleada aquí y contiene numerosos ejemplos resueltos. Ejercicios Algunos de los ejercicios puedes probarlos en el portal y juez en línea “Acepta el reto” (https://www.aceptaelreto.com). Son los que aparecen marcados con el icono seguido del número de problema dado en el portal. 1. Representar gráficamente la relación P ) Q para el siguiente conjunto de predicados: a) P1 ⌘ x > 0 b) P2 ⌘ (x > 0) ^ (y > 0) c) P3 ⌘ (x > 0) _ (y > 0) d ) P4 ⌘ y 0 e) P5 ⌘ (x 0) ^ (y 0) Indicar cuáles de dichos predicados son incomparables (P es incomparable con Q si P 6) Q y Q 6) P ). 2. ( ACR247)Construir un predicado ord (a, n) que exprese que el vector int a[n] está ordenado crecientemente. 3. Generalizar el predicado anterior a otro ord (a, i, j, n) que exprese que el subvector a[i..j] de int a[n] está ordenado crecientemente. ¿Tiene sentido ord (a, 7, 6, 10)? 4. Construir un predicado perm(a, b, n), donde a y b son vectores de longitud n, que exprese que el vector b contiene una permutación de los elementos de a. 5. Especificar un procedimiento o función que ordene un vector de longitud n crecien- temente. 6. Especificar un procedimiento o función que sustituya en un vector int a[n] todas las apariciones del valor x por el valor y. 7. ( ACR152)Dada una colección de valores, se denomina moda al valor que más veces aparece repetido en dicha colección. Queremos especificar una función que, dado un vector a[n] de enteros con n 1, devuelva la moda del vector. 8. Un vector int a[n], con n 0, se dice que es gaspariforme si todas sus sumas parciales son no negativas y la suma total es igual a cero. Se llama suma parcial a toda suma a + · · · + a[i], con 0  i < n. Especificar una función que, dados a y n, decida si a es o no gaspariforme. ¿Qué debe devolver la función cuando n = 0? 9. Especificar un algoritmo que calcule la imagen especular de un vector. Precisando, el valor que estaba en a pasa a estar en a[n 1], el que estaba en a pasa a estar en a[n 2], etc. Permitir el caso n = 0. Facultad de Informática - UCM 24 Capítulo 2. Especificación de algoritmos 10. Dado un vector int a[n], con n 0, formalizar cada una de las siguientes afirmaciones: a) El vector a es estrictamente creciente. b) Todos los valores de a son distintos. c) Todos los valores de a son iguales. d ) Si a contiene un 0, entonces a también contendrá un 1. e) No hay dos elementos contiguos de a que sean iguales. f ) El máximo de a solo aparece una vez en a. g) El resultado l es la longitud máxima de un segmento constante en a. h) Todos los valores de a son números primos. i) El número de elementos pares de a es igual al número de elementos impares. j ) El resultado p es el producto de todos los valores positivos de a. k ) El vector a contiene un cuadrado perfecto. 11. Especificar una función que dado un natural n, devuelva la raíz cuadrada entera de n. 12. Especificar una función que dados a > 0 y b > 1, devuelva el logaritmo entero en base b de a. 13. Dado un vector int a[n], con n 1, expresar en lenguaje natural las siguientes postcondiciones: a) b = (9w : 0  w < n : a[w] = 2 ⇥ w) b) m = (# w : 1  w < n : a[w 1] < a[w]) c) m = (máx u, v : 0  u < v < n : a[u] + a[v]) d ) l = (máx u, v : 0  u  v < n ^ (8w : u  w  v : a[w] = 0) : v u + 1) P e) r = (máx u, v : 0  u  v < n : ( w : u  w  v : a[w])) Q f ) p = ( u, v : 0  u < v < n : a[v] a[u]) 14. (Martí Oliet et al. (2012)) Dado x un vector de enteros, r y m dos enteros, y n 1 un natural, formalizar cada una de las siguientes afirmaciones: x[0..n) contiene el cuadrado de un número. r es el producto de todos los elementos positivos en x[0..n). m es el resultado de sumar los valores en las posiciones pares de x[0..n) y restar los valores en las posiciones impares. r es el número de veces que m aparece en x[0..n). 15. (Martí Oliet et al. (2012)) Comparar la fuerza lógica de los siguiente pares de predi- cados: a) P = x 0, Q=x 0!y 0. b) P = x 0_y 0, Q = x + y = 0. c) P = x < 0, Q = x2 + y 2 = 9. d) P = x 1!x 0, Q=x 1. Fundamentos de Algoritmia Ejercicios... 25 16. (Martí Oliet et al. (2012)) Especificar funciones que resuelvan los siguientes proble- mas: a) Decidir si un entero es el factorial de algún número natural. b) Calcular el número de ceros que aparecen en un vector de enteros. c) Calcular el producto escalar de dos vectores de reales. d ) Calcular la posición del máximo del vector no vacío de enteros v[0..n). e) Calcular la primera posición en la que aparece el máximo del vector no vacío v[0..n). 17. (Martí Oliet et al. (2012)) Especificar una función que, dado un vector de números enteros, devuelva un valor booleano indicando si el valor de alguno de los elementos del vector es igual a la suma de todos los elementos que le preceden en el vector. 18. (Martí Oliet et al. (2012)) La fórmula de Taylor-Maclaurin proporciona la siguiente serie convergente para calcular el seno de un ángulo x expresado en radianes: 1 X ( 1)n seno(x) = x2n+1. (2n + 1)! n=0 Por esta razón, para aproximar el seno de x con un error menor que un número real ( 1)k positivo ✏ basta encontrar un número natural k tal que (2k+1)! x2k+1 < ✏ y entonces k 1 X ( 1)n senoAprox (x) = x2n+1. (2n + 1)! n=0 Especificar formalmente una función que, dados los valores de x y ✏ > 0, calcule el valor aproximado del seno de x con un error menor que ✏. 19. Diremos que una posición de un vector de enteros es fija si el valor contenido en dicha posición coincide con la posición. Especificar una función hayFija que, dado un vector v[0..n) de enteros estrictamente creciente, indique si hay alguna posición fija en el vector. 20. ( ACR171)Dado un vector de enteros v, el índice i es mirador si v[i] es el mayor elemento de v[i..n-1]. Especifica una función que reciba un vector y calcule el número de miradores que tiene. 21. ( ACR221)Especifica una función que reciba un vector de enteros y devuelva un valor booleano indicando si se puede dividir en dos partes (alguna de ellas quizá vacía) donde la primera parte tenga sólo números pares y la segunda números impares. 22. ( ACR242)Especifica una función que reciba un vector de enteros y devuelva el resultado de sumar la multiplicación de todas las parejas de números v[i], v[j] (con i distinto de j). 23. ( ACR219)Especifica una función que reciba un vector y calcule cuántos números pares tiene. 24. ( ACR224)Especifica una función que reciba un vector y calcule, si existe, la posición del mismo que es igual a la suma de los elementos que tiene a la izquierda. Si hay más de uno, debe devolverse el situado más a la derecha. Facultad de Informática - UCM