Overené funkčné programovanie v Agde

Recenzie čitateľov

Kniha je chválená ako prístupný úvod do závislých typov pomocou Agda, najmä pre praktické dokazovanie tvrdení. Má však výrazné nedostatky v prehľadnosti, organizácii a prezentácii, čo ovplyvňuje jej celkovú účinnosť.

Najprístupnejší úvod do závislých typov v praxi, najmä pre Agdu.

Pripravuje čitateľov na pokročilejšie knihy o tejto téme.

(na základe 4 čitateľských recenzií)

Pôvodný názov:

Verified Functional Programming in Agda

Obsah knihy:

Agda je pokročilý programovací jazyk založený na teórii typov. Typový systém jazyka Agda je dostatočne expresívny na to, aby podporoval úplnú funkcionálnu verifikáciu programov v dvoch štýloch.

Pri externej verifikácii píšeme čisté funkcionálne programy a potom o nich píšeme dôkazy vlastností. Dôkazy sú samostatné externé artefakty, zvyčajne využívajúce štrukturálnu indukciu. Pri internej verifikácii špecifikujeme vlastnosti programov prostredníctvom bohatých typov pre samotné programy.

To si často vyžaduje zahrnutie dôkazov vo vnútri kódu, aby sme kontrole typov ukázali, že zadané vlastnosti platia. Možnosť dokazovať vlastnosti programov v týchto dvoch štýloch je hlbokým prínosom pre prax programovania, pretože dáva programátorom možnosť zaručiť neprítomnosť chýb, a tým zlepšiť kvalitu softvéru viac, ako bolo predtým možné. Verifikované funkcionálne programovanie v Agde je prvá kniha, ktorá poskytuje systematický výklad externej a internej verifikácie v Agde, vhodný pre vysokoškolských študentov informatiky.

Nepredpokladá sa žiadna znalosť funkcionálneho programovania alebo počítačom overovaných dôkazov. Kniha začína úvodom do funkcionálneho programovania prostredníctvom známych príkladov, ako sú booleány, prirodzené čísla a zoznamy, a techník externej verifikácie. Vnútorná verifikácia sa posudzuje na príkladoch vektorov, binárnych vyhľadávacích stromov a Braunových stromov.

Súčasťou je aj pokročilejší materiál o výpočtoch na úrovni typov, explicitnom zdôvodňovaní ukončenia a normalizácii pomocou vyhodnocovania. Kniha obsahuje aj stredne rozsiahlu prípadovú štúdiu o Huffmanovom kódovaní a dekódovaní.