Especificación, Verificación y Derivación Formal de Programas

Desde prácticamente los inicios de la Informática, una de las líneas constantes de trabajo ha ido en la dirección de reducir el número de errores de programación o de mitigar sus consecuencias. Actualmente, existen los conocimientos, los métodos y la tecnología para que se pudiera construir software totalmente fiable, es decir (prácticamente) libre de errores. Prueba de ello es, por ejemplo, el software de la red de transporte parisina que se describe en el capítulo introductorio de este libro. Otra prueba es que en los últimos 10 o 15 años no haya habido, prácticamente, accidentes graves provocados por fallos de software. Esto es gracias a que, en el caso del software crítico, del que pueden depender las vidas de personas, si se utiliza toda la tecnología necesaria para garantizar su fiabilidad. ¿Por qué, entonces, no se aplican estas mismas técnicas en el desarrollo del software no crítico? Uno de los principales motivos es que los desarrolladores de software no cuentan con la formación básica necesaria para utilizar las técnicas y herramientas que garantizan la fiabilidad del software.

Este libro suministra material para un curso de formación introductorio en técnicas básicas de especificación, transformación y verificación de programas, que están detrás de los métodos que se utilizan para la construcción de software fiable. Presentamos, e ilustramos con ejemplos y ejercicios, una colección de métodos formales básicos de especificación de programas y tipos de datos, de verificación de programas imperativos y recursivos sencillos, de transformación de especificaciones (y/o programas) recursivos en iterativos y de derivación formal de programas, tanto iterativos como recursivos. Cada capítulo del libro contiene ejemplos completamente desarrollados, y varias secciones con ejercicios propuestos de similar dificultad a los desarrollados en las secciones precedentes, incluyendo una sección final de ejercicios de recopilación. Así mismo, cada capítulo incluye una sección de notas bibliográficas donde se pueden encontrar reseñas históricas y referencias interesantes.

Con este libro pretendemos contribuir a un reto que la comunidad internacional ya ha asumido: La industria del software debe evolucionar hacia producir aplicaciones totalmente fiables, para lo cual es fundamental que los desarrolladores de software cuenten con la formación científico-técnica que les capacite para usar y desarrollar las herramientas y técnicas necesarias para construir software totalmente fiable.