Ověřené funkční programování v Agdě

Recenze čtenářů

Recenze knihy vyzdvihují její přístupnost a praktický přístup k závislým typům pomocí Agdy a zdůrazňují její vhodnost pro začátečníky, a to i přes některé nedostatky v přehlednosti a organizaci. Zatímco mnoho čtenářů ji považuje za vynikající pro výuku Agdy a dokazování teorémů, objevuje se kritika týkající se její struktury, přehlednosti a prezentace, zejména ve verzi pro Kindle.

⬤ Přístupný úvod do problematiky závislých typů v praktickém prostředí s využitím Agdy.
⬤ Připraví čtenáře na pokročilejší látku o teorii typů a dokazování vět.
⬤ Obsahuje velké množství jednoduchých důkazů a praktických příkladů.
⬤ Vhodný pro čtenáře bez předchozích znalostí logiky nebo teorie typů, což zvyšuje jeho dosah.

⬤ Chybí teoretické pokrytí závislých typů.
⬤ V některých částech není kladen důraz na obecné pojmy před ponořením se do detailů.
⬤ Problémy s přehledností výkladu a uspořádání kapitol; některé body se příliš opakují, zatímco jiné jsou nedostatečně vysvětleny.
⬤ Verze pro Kindle má špatné rozvržení, nedostatečné odsazení odstavců a problémy se zarovnáním zdrojového kódu.

(na základě 4 hodnocení čtenářů)

Původní název:

Verified Functional Programming in Agda

Obsah knihy:

Agda je pokročilý programovací jazyk založený na teorii typů. Typový systém jazyka Agda je dostatečně expresivní, aby podporoval plnou funkcionální verifikaci programů, a to ve dvou stylech.

Při externí verifikaci píšeme čisté funkcionální programy a pak o nich píšeme důkazy vlastností. Důkazy jsou samostatnými externími artefakty, obvykle využívajícími strukturní indukci. Při interní verifikaci specifikujeme vlastnosti programů prostřednictvím bohatých typů pro samotné programy.

To často vyžaduje zahrnutí důkazů uvnitř kódu, abychom ukázali typovému kontroléru, že zadané vlastnosti platí. Možnost dokazovat vlastnosti programů v těchto dvou stylech je hlubokým přínosem pro programátorskou praxi a dává programátorům možnost zaručit nepřítomnost chyb, a tím zlepšit kvalitu softwaru více, než bylo dříve možné. Verifikované funkcionální programování v Agdě je první knihou, která poskytuje systematický výklad vnější a vnitřní verifikace v Agdě, vhodný pro vysokoškolské studenty informatiky.

Nepředpokládá se žádná znalost funkcionálního programování ani počítačem ověřovaných důkazů. Kniha začíná úvodem do funkcionálního programování prostřednictvím známých příkladů, jako jsou booleány, přirozená čísla a seznamy, a technik pro vnější verifikaci. Vnitřní verifikace je probírána na příkladech vektorů, binárních vyhledávacích stromů a Braunových stromů.

Součástí je také pokročilejší materiál o výpočtech na úrovni typů, explicitním zdůvodnění ukončení a normalizaci pomocí vyhodnocení. Kniha obsahuje také středně rozsáhlou případovou studii o Huffmanově kódování a dekódování.