Teórie programovania: Teórie programovania: Život a dielo Tonyho Hoarea

Recenzie čitateľov

Momentálne nie sú žiadne recenzie čitateľov. Hodnotenie je založené na 2 hlasoch.

Pôvodný názov:

Theories of Programming: The Life and Works of Tony Hoare

Obsah knihy:

Sir Tony Hoare mal obrovský vplyv na počítačovú vedu, od algoritmu Quicksort až po vedu o vývoji softvéru, súbežnosti a overovaní programov. Jeho prínos bol široko uznávaný: v roku 1980 mu bola udelená Turingova cena ACM, v roku 2000 dostal Kjótsku cenu od nadácie Inamori a v roku 2000 ho anglická kráľovná Alžbeta II. pasovala na rytiera za "služby v oblasti vzdelávania a počítačovej vedy".

Táto kniha predstavuje podstatu jeho rôznych prác - hľadanie efektívnych abstrakcií - tak jeho vlastnými slovami, ako aj v kapitolách napísaných poprednými odborníkmi v tejto oblasti vrátane mnohých jeho výskumných spolupracovníkov. Okrem toho tento zväzok obsahuje životopisný materiál, jeho prednášku o Turingovej cene, prepis rozhovoru a niektoré jeho zásadné práce.

Hoare vo svojej základnej práci "An Axiomatic Basis for Computer Programming" predstavil svoj prístup, všeobecne známy ako Hoare Logic, na dokazovanie správnosti programov pomocou logických tvrdení. Hoareho logika a následný vývoj sa stali základom širokej škály overovania softvéru. Hoare zohral kľúčovú úlohu pri navrhovaní iniciatívy Verified Software Initiative, medzinárodného projektu spolupráce zameraného na vedecké výzvy v oblasti rozsiahlej verifikácie softvéru, ktorý zahŕňa teórie, nástroje a experimenty.

Príspevky Tonyho Hoareho k teórii a praxi súbežných softvérových systémov sú rovnako pôsobivé. Procesná algebra s názvom Communicating Sequential Processes (CSP) bola jednou zo základných paradigiem, a to ako matematická teória na zdôvodnenie súbežných výpočtov, ako aj ako základ pre programovací jazyk occam. CSP slúžila ako rámec na skúmanie viacerých myšlienok v denotačnej sémantike, ako sú powerdomains, ako aj pojmov abstrakcie a zjemňovania. Je základom pre sériu priemyselne silných nástrojov, ktoré sa využívajú v širokom spektre aplikácií.

Táto kniha predstavuje aj Hoareho prácu za posledných niekoľko desaťročí. Tieto práce zahŕňajú rigorózny prístup k špecifikáciám v praxi softvérového inžinierstva vrátane procedurálnych a dátových abstrakcií, spresňovania údajov a modulárnej teórie návrhov. V poslednom čase spolupracoval so spolupracovníkmi na vývoji zjednocujúcich teórií programovania (UTP). Ich cieľom je identifikovať spoločné algebraické teórie, ktoré sú jadrom sekvenčných, súbežných, reaktívnych a kyberneticko-fyzických výpočtov.