A programozás elméletei: Tony Hoare élete és művei

Olvasói vélemények

Jelenleg nincsenek olvasói vélemények. Az értékelés 2 olvasói szavazat alapján történt.

Eredeti címe:

Theories of Programming: The Life and Works of Tony Hoare

Könyv tartalma:

Sir Tony Hoare óriási hatással volt a számítástechnikára, a Quicksort algoritmustól kezdve a szoftverfejlesztés, az egyidejűség és a programellenőrzés tudományáig. Hozzájárulását széles körben elismerték: 1980-ban megkapta az ACM Turing-díját, 2000-ben az Inamori Alapítvány Kiotói-díját, 2000-ben pedig II. Erzsébet angol királynő lovaggá ütötte "az oktatás és a számítástechnika szolgálataiért".

Ez a könyv különböző munkáinak lényegét - a hatékony absztrakciók keresését - mutatja be mind saját szavaival, mind a terület vezető szakértőinek - köztük számos kutatótársának - által írt fejezetekkel. A kötet emellett életrajzi anyagot, a Turing-díjjal kapcsolatos előadását, egy interjú leiratát és néhány korszakalkotó tanulmányát is tartalmazza.

Hoare "An Axiomatic Basis for Computer Programming" (A számítógépes programozás axiomatikus alapja) című alapművében bemutatta a Hoare-logika néven ismert megközelítését, amely a programok helyességét logikai állítások segítségével bizonyítja. A Hoare-logika és az azt követő fejlesztések a legkülönfélébb szoftverellenőrzési erőfeszítések alapját képezték. Hoare jelentős szerepet játszott a Verified Software Initiative (Ellenőrzött Szoftver Kezdeményezés) létrehozásában, amely egy olyan nemzetközi együttműködési projekt, amely a nagyszabású szoftverellenőrzés tudományos kihívásaira irányul, és elméleteket, eszközöket és kísérleteket foglal magában.

Tony Hoare hozzájárulása az egyidejű szoftverrendszerek elméletéhez és gyakorlatához ugyanilyen lenyűgöző. A kommunikáló szekvenciális folyamatok (CSP) nevű folyamatalgebra az egyik alapvető paradigma volt, mind az egyidejű számítások matematikai elmélete, mind az occam programozási nyelv alapja. A CSP szolgált keretként a denotációs szemantika számos gondolatának, például a powerdomains, valamint az absztrakció és a finomítás fogalmainak feltárásához. Ez az alapja egy sor ipari szintű eszköznek, amelyeket alkalmazások széles körében alkalmaztak.

Ez a könyv Hoare elmúlt évtizedekben végzett munkásságát is bemutatja. Ezek a munkák magukban foglalják a specifikációk szigorú megközelítését a szoftverfejlesztés gyakorlatában, beleértve az eljárás- és adatabsztrakciókat, az adatfinomítást és a tervek moduláris elméletét. Újabban munkatársaival együtt dolgozott a programozás egységesítő elméleteinek (Unifying Theories of Programming, UTP) kidolgozásán. Céljuk a szekvenciális, egyidejű, reaktív és kiber-fizikai számítások középpontjában álló közös algebrai elméletek azonosítása.