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

Recenze čtenářů

Kniha je chválena jako přístupný úvod do závislých typů pomocí Agdy, zejména pro praktické dokazování vět. Má však výrazné nedostatky v přehlednosti, organizaci a prezentaci, což ovlivňuje její celkovou účinnost.

Nejpřístupnější úvod do závislých typů v praxi, zejména pro Agdu.

Připraví čtenáře na pokročilejší knihy o tomto tématu.

(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í.