Teorie della programmazione: La vita e le opere di Tony Hoare

Recensioni dei lettori

Attualmente non ci sono recensioni dei lettori. La valutazione si basa su 2 voti.

Titolo originale:

Theories of Programming: The Life and Works of Tony Hoare

Contenuto del libro:

Sir Tony Hoare ha avuto un'enorme influenza sull'informatica, dall'algoritmo Quicksort alla scienza dello sviluppo del software, della concorrenza e della verifica dei programmi. I suoi contributi sono stati ampiamente riconosciuti: è stato insignito del Premio Turing dell'ACM nel 1980, del Premio Kyoto della Fondazione Inamori nel 2000 e nel 2000 è stato nominato cavaliere per i "servizi resi all'istruzione e all'informatica" dalla Regina Elisabetta II d'Inghilterra.

Questo libro presenta l'essenza dei suoi vari lavori - la ricerca di astrazioni efficaci - sia con le sue parole che con i capitoli scritti dai maggiori esperti del settore, tra cui molti dei suoi collaboratori di ricerca. Inoltre, il volume contiene materiale biografico, la sua conferenza al premio Turing, la trascrizione di un'intervista e alcuni dei suoi articoli fondamentali.

L'articolo fondamentale di Hoare, "An Axiomatic Basis for Computer Programming", presentava il suo approccio, comunemente noto come Logica di Hoare, per dimostrare la correttezza dei programmi utilizzando asserzioni logiche. La logica di Hoare e gli sviluppi successivi hanno costituito la base di un'ampia gamma di iniziative di verifica del software. Hoare è stato determinante nel proporre la Verified Software Initiative, un progetto cooperativo internazionale diretto alle sfide scientifiche della verifica del software su larga scala, che comprende teorie, strumenti ed esperimenti.

I contributi di Tony Hoare alla teoria e alla pratica dei sistemi software concorrenti sono altrettanto notevoli. L'algebra dei processi chiamata Communicating Sequential Processes (CSP) è stata uno dei paradigmi fondamentali, sia come teoria matematica per ragionare sulla computazione concorrente sia come base per il linguaggio di programmazione occam. CSP è servito come quadro di riferimento per l'esplorazione di diverse idee di semantica denotativa, come i domini di potenza, e di nozioni di astrazione e raffinamento. È la base per una serie di strumenti di livello industriale che sono stati utilizzati in un'ampia gamma di applicazioni.

Questo libro presenta anche il lavoro svolto da Hoare negli ultimi decenni. Questi lavori includono un approccio rigoroso alle specifiche nella pratica dell'ingegneria del software, comprese le astrazioni procedurali e di dati, il raffinamento dei dati e una teoria modulare dei progetti. Più recentemente, ha lavorato con alcuni collaboratori per sviluppare teorie unificanti della programmazione (UTP). Il loro obiettivo è identificare le teorie algebriche comuni che sono alla base delle computazioni sequenziali, concorrenti, reattive e cyber-fisiche.