Teorías de la programación: Vida y obra de Tony Hoare

Título original:

Theories of Programming: The Life and Works of Tony Hoare

Contenido del libro:

Sir Tony Hoare ha tenido una enorme influencia en la informática, desde el algoritmo Quicksort hasta la ciencia del desarrollo de software, la concurrencia y la verificación de programas. Sus contribuciones han sido ampliamente reconocidas: recibió el Premio Turing de la ACM en 1980, el Premio Kyoto de la Fundación Inamori en 2000 y fue nombrado caballero por sus "servicios a la educación y la informática" por la Reina Isabel II de Inglaterra en 2000.

Este libro presenta la esencia de sus diversos trabajos -la búsqueda de abstracciones eficaces- tanto en sus propias palabras como en capítulos escritos por destacados expertos en la materia, entre ellos muchos de sus colaboradores en la investigación. Además, este volumen contiene material biográfico, su conferencia del premio Turing, la transcripción de una entrevista y algunos de sus artículos fundamentales.

El artículo fundacional de Hoare "An Axiomatic Basis for Computer Programming" (Una base axiomática para la programación informática) presentó su enfoque, conocido comúnmente como Lógica de Hoare, para demostrar la corrección de los programas mediante aserciones lógicas. La Lógica de Hoare y sus desarrollos posteriores han constituido la base de una amplia variedad de esfuerzos de verificación de software. Hoare desempeñó un papel decisivo en la propuesta de la Verified Software Initiative, un proyecto de cooperación internacional dirigido a los retos científicos de la verificación de software a gran escala, que abarca teorías, herramientas y experimentos.

Las contribuciones de Tony Hoare a la teoría y la práctica de los sistemas de software concurrentes son igualmente impresionantes. El álgebra de procesos denominada Communicating Sequential Processes (CSP) ha sido uno de los paradigmas fundamentales, tanto como teoría matemática para razonar sobre computación concurrente como base del lenguaje de programación occam. CSP sirvió de marco para explorar varias ideas de la semántica denotacional, como los dominios de potencia, así como las nociones de abstracción y refinamiento. Es la base de una serie de herramientas industriales que se han empleado en una amplia gama de aplicaciones.

Este libro también presenta los trabajos de Hoare en las últimas décadas. Estos trabajos incluyen un enfoque riguroso de las especificaciones en la práctica de la ingeniería del software, incluidas las abstracciones procedimentales y de datos, el refinamiento de datos y una teoría modular de los diseños. Más recientemente, ha trabajado con colaboradores para desarrollar Teorías Unificadoras de la Programación (UTP). Su objetivo es identificar las teorías algebraicas comunes que se encuentran en el núcleo de los cálculos secuenciales, concurrentes, reactivos y ciberfísicos.