Descripción
Algoritmos y Estructuras de Datos con Programas Verificados en Dafny (2ª Edición)
Resumen del libro
Esta obra ofrece un tratamiento avanzado y riguroso de las estructuras de datos y los métodos algorítmicos, utilizando el lenguaje de verificación formal Dafny como herramienta central. El lector encontrará una exposición detallada de técnicas eficientes de programación, acompañadas de programas verificados que garantizan su corrección. El libro está diseñado para servir como texto base en cursos superiores de programación, combinando teoría, práctica y demostración formal.
¿De qué trata?
El libro aborda una amplia variedad de estructuras de datos y métodos algorítmicos, organizados para cubrir dos semestres avanzados de programación. En la primera parte, se centra en estructuras de datos eficientes, como árboles balanceados, montículos y tablas hash, explicando su implementación y propiedades. En la segunda parte, explora métodos algorítmicos fundamentales, incluyendo algoritmos de ordenación, búsqueda, divide y vencerás, programación dinámica y algoritmos voraces.
Una característica distintiva es el uso de Dafny, un lenguaje que permite especificar y verificar formalmente la corrección de los programas. Cada algoritmo y estructura se presenta junto con su especificación formal y su demostración de corrección, lo que proporciona un nivel de rigor poco común en los textos de programación. La obra asume conocimientos previos sólidos de programación, incluyendo recursión, estructuras de datos lineales y nociones de programación orientada a objetos.
Temas principales
- Estructuras de datos eficientes: árboles balanceados (AVL, rojo-negro), montículos, colas de prioridad, tablas hash y grafos.
- Métodos algorítmicos: divide y vencerás, programación dinámica, algoritmos voraces, backtracking y algoritmos de ordenación avanzados.
- Especificación y verificación formal de programas mediante el lenguaje Dafny.
- Análisis de complejidad temporal y espacial de algoritmos.
- Implementación de programas correctos por construcción, con demostraciones formales de propiedades.
¿Para quién está recomendado?
Está dirigido a estudiantes universitarios de ingeniería informática, matemáticas o ciencias de la computación que hayan completado al menos dos o tres semestres de asignaturas de programación. También es adecuado para profesionales que deseen profundizar en la verificación formal de programas y en algoritmos avanzados. Se recomienda tener conocimientos previos o simultáneos de programación funcional, lógica, matemática discreta y fundamentos de especificación formal.
Qué aporta este libro
- Un enfoque riguroso que combina teoría algorítmica con verificación formal, garantizando la corrección de los programas.
- Más de 400 páginas de contenido avanzado, con ejemplos prácticos y programas verificados en Dafny.
- Preparación para abordar problemas complejos de programación con un alto nivel de abstracción y precisión.
- Base sólida para la investigación o el desarrollo en áreas que requieren software crítico y fiable.
Ficha técnica
- Autor: Ricardo Peña Marí
- Editorial: Ibergarceta Publicaciones S.L.
- Idioma: Español
- Tema: Ingeniería mecánica y de materiales, Algoritmos y estructuras de datos
- Colección: Ciclos Formativos
- Encuadernación: Bolsillo
- Fecha de edición: septiembre de 2023
- Número de páginas: 400
- Peso: 6774 g
Valoración editorial
Esta segunda edición consolida un texto de referencia para cursos avanzados de programación, destacando por su enfoque en la verificación formal. La inclusión de Dafny como lenguaje de trabajo no es un mero añadido, sino que vertebra toda la exposición, ofreciendo al lector una metodología para construir programas correctos desde su especificación. Resulta especialmente valiosa para aquellos que buscan un tratamiento profundo y formal de los algoritmos, más allá de la mera implementación práctica.