Teorie programowania: Życie i twórczość Tony'ego Hoare'a

Opinie czytelników

Obecnie brak opinii czytelników. Ocena opiera się na 2 głosach.

Oryginalny tytuł:

Theories of Programming: The Life and Works of Tony Hoare

Zawartość książki:

Sir Tony Hoare wywarł ogromny wpływ na informatykę, od algorytmu Quicksort po naukę o tworzeniu oprogramowania, współbieżności i weryfikacji programów. Jego wkład został powszechnie doceniony: w 1980 roku otrzymał Nagrodę Turinga przyznawaną przez ACM, w 2000 roku Nagrodę Kyoto przyznawaną przez Fundację Inamori, a w 2000 roku został pasowany na rycerza za "zasługi dla edukacji i informatyki" przez angielską królową Elżbietę II.

Niniejsza książka przedstawia istotę jego różnych prac - poszukiwanie skutecznych abstrakcji - zarówno jego własnymi słowami, jak i rozdziałami napisanymi przez czołowych ekspertów w tej dziedzinie, w tym wielu jego współpracowników badawczych. Ponadto tom ten zawiera materiały biograficzne, jego wykład o nagrodzie Turinga, transkrypcję wywiadu i niektóre z jego przełomowych artykułów.

Fundamentalny artykuł Hoare'a "An Axiomatic Basis for Computer Programming" przedstawił jego podejście, powszechnie znane jako Hoare Logic, do dowodzenia poprawności programów za pomocą twierdzeń logicznych. Logika Hoare'a i jej późniejsze rozwinięcia stały się podstawą wielu różnych działań związanych z weryfikacją oprogramowania. Hoare odegrał kluczową rolę w zaproponowaniu Verified Software Initiative, międzynarodowego projektu współpracy ukierunkowanego na naukowe wyzwania związane z weryfikacją oprogramowania na dużą skalę, obejmującego teorie, narzędzia i eksperymenty.

Wkład Tony'ego Hoare'a w teorię i praktykę współbieżnych systemów oprogramowania jest równie imponujący. Algebra procesów zwana Communicating Sequential Processes (CSP) była jednym z podstawowych paradygmatów, zarówno jako teoria matematyczna do rozumowania o obliczeniach współbieżnych, jak i podstawa języka programowania occam. CSP posłużył jako ramy do zbadania kilku pomysłów w semantyce denotacyjnej, takich jak domeny mocy, a także pojęcia abstrakcji i wyrafinowania. Jest to podstawa dla szeregu narzędzi przemysłowych, które zostały wykorzystane w szerokim zakresie zastosowań.

Książka ta przedstawia również prace Hoare'a z ostatnich kilku dekad. Prace te obejmują rygorystyczne podejście do specyfikacji w praktyce inżynierii oprogramowania, w tym abstrakcje proceduralne i danych, udoskonalanie danych i modułową teorię projektów. Ostatnio, wraz ze współpracownikami, pracował nad rozwojem ujednoliconych teorii programowania (UTP). Ich celem jest zidentyfikowanie wspólnych teorii algebraicznych, które leżą u podstaw obliczeń sekwencyjnych, współbieżnych, reaktywnych i cyberfizycznych.