Teorii ale programării: Viața și opera lui Tony Hoare

Recenzii ale cititorilor

În prezent, nu există recenzii ale cititorilor. Evaluarea se bazează pe 2 voturi.

Titlul original:

Theories of Programming: The Life and Works of Tony Hoare

Conținutul cărții:

Sir Tony Hoare a avut o influență enormă asupra informaticii, de la algoritmul Quicksort la știința dezvoltării de software, a concurenței și a verificării programelor. Contribuțiile sale au fost recunoscute pe scară largă: a primit Premiul Turing al ACM în 1980, Premiul Kyoto al Fundației Inamori în 2000 și a fost făcut cavaler pentru "servicii aduse educației și informaticii" de către Regina Elisabeta a II-a a Angliei în 2000.

Această carte prezintă esența diverselor sale lucrări - căutarea abstractizărilor eficiente - atât în propriile sale cuvinte, cât și în capitole scrise de experți de marcă în domeniu, inclusiv de mulți dintre colaboratorii săi de cercetare. În plus, acest volum conține materiale biografice, prelegerea sa pentru premiul Turing, transcrierea unui interviu și câteva dintre lucrările sale fundamentale.

Lucrarea fundamentală a lui Hoare "An Axiomatic Basis for Computer Programming" (O bază axiomatică pentru programarea calculatoarelor) a prezentat abordarea sa, cunoscută sub numele de Hoare Logic, pentru dovedirea corectitudinii programelor prin utilizarea aserțiunilor logice. Hoare Logic și dezvoltările ulterioare au stat la baza unei mari varietăți de eforturi de verificare a software-ului. Hoare a avut un rol esențial în propunerea Inițiativei pentru software verificat, un proiect internațional de cooperare care vizează provocările științifice ale verificării software-ului la scară largă, cuprinzând teorii, instrumente și experimente.

Contribuțiile lui Tony Hoare la teoria și practica sistemelor software concurente sunt la fel de impresionante. Algebra de procese numită Communicating Sequential Processes (CSP) a fost una dintre paradigmele fundamentale, atât ca teorie matematică pentru raționamentul despre calculul concurent, cât și ca bază pentru limbajul de programare occam. CSP a servit drept cadru pentru explorarea mai multor idei în semantica denotațională, cum ar fi powerdomains, precum și a noțiunilor de abstractizare și rafinare. CSP reprezintă baza pentru o serie de instrumente industriale care au fost utilizate într-o gamă largă de aplicații.

Această carte prezintă, de asemenea, lucrările lui Hoare din ultimele câteva decenii. Aceste lucrări includ o abordare riguroasă a specificațiilor în practica ingineriei software, inclusiv abstracții procedurale și de date, rafinarea datelor și o teorie modulară a proiectelor. Mai recent, el a lucrat cu colaboratori pentru a dezvolta teorii unificatoare ale programării (UTP). Scopul lor este de a identifica teoriile algebrice comune care stau la baza calculelor secvențiale, concurente, reactive și cyber-fizice.