Prólogo

Capítulo 1. Especificación de algoritmos.

1.1 Introducción.

1.2 Ejercicios resueltos.

1.3 Ejercicios propuestos.

Capítulo 2. Verificación.

2.1 Introducción

2.1.1 Reglas básicas de verificación

2.1.2 Precondición más débil

2.1.3 Reglas específicas

2.1.4 Verificación de algoritmos recursivos

2.2 Ejercicios resueltos

2.3 Ejercicios propuestos

Capítulo 3. Análisis de complejidad.

3.1 Introducción

3.2 Ejercicios resueltos

3.3 Ejercicios propuestos

Capítulo 4. Derivación de algoritmos iterativos.

4.1 Introducción

4.2 Ejercicios resueltos

4.3 Ejercicios propuestos

Capítulo 5. Derivación de algoritmos recursivos.

5.1 Introducción

5.1.1 Análisis por casos y composición

5.1.2 Técnicas de inmersión

5.1.3 Técnica de desplegado y plegado

5.1.4 Transformación de recursivo lineal e iterativo

5.2 Ejercicios resueltos

5.3 Ejercicios propuestos

Bibliografía.

Enfoque:

- Aunque los temas relacionados con la especificación y verificación formal de programas no gozan de mucha popularidad, es importante su inclusión en los temarios, sobre todo haciendo más hincapié en la derivación de programas a partir de su especificación, de forma que se obtiene un algoritmo correcto por construcción. - Con el presente libro se intenta contribuir a paliar este déficit, pero además en un formato apropiado para los alumnos que demandan como complemento a los "libros de teoría" y a los apuntes de clase, un libro de ejercicios resueltos.

-De esta forma, cada capítulo comienza con una breve introducción cuyo objetivo es repasar los conceptos principales y fijar las notaciones que se utilizan en el desarrollo posterior de las soluciones de los ejercicios, pero no supone un tratamiento detallado del tema, para el cual se remite a algunos libros de teoría, como el de Ricardo Peña: "Diseño de programas".

La parte principal de cada capítulo consiste en una serie de ejercicios resueltos de dificultad creciente. Además, al final de cada capítulo se proponen nuevos ejercicios para resolver por el lector.

- En la presentación de las soluciones a los ejercicios resueltos se ve directamente una solución que funciona, pero ya no hay ocasión de ver los posibles pasos fallidos que uno ha podido dar antes de llegar a la solución, por lo que se anima a los lectores a intentar llegar a una solución por su cuenta, para ver cuáles son los pasos que hay que dar y con qué opciones se enfrenta uno en cada paso. Sin embargo, la idea de la verificación es que uno tiene tanto la especificación como el programa y se comprueba "a posteriori" que en efecto el programa cumpla su especificación. Para ello se utiliza una serie de reglas que se presentan e ilustran en los dos primeros capítulos. En el proceso de derivación se usan esas mismas reglas, pero de una forma completamente distinta, que es la que se ilustra en los capítulos 4 y 5. El capítulo intermedio, el 3, se dedica a introducir los conceptos básicos para analizar el coste de un programa, puesto que este ingrediente también es útil para construir programas que además de correctos sean eficientes.