Overené funkčné programovanie v Agde

Recenzie čitateľov

V recenziách knihy sa vyzdvihuje jej prístupnosť a praktický prístup k závislým typom pomocou Agda, pričom sa zdôrazňuje jej vhodnosť pre začiatočníkov napriek niektorým nedostatkom v prehľadnosti a organizácii. Hoci mnohí čitatelia ju považujú za vynikajúcu na učenie sa Agda a dokazovania tvrdení, objavujú sa kritické pripomienky týkajúce sa jej štruktúry, prehľadnosti a prezentácie, najmä vo verzii pre Kindle.

⬤ Prístupný úvod do závislých typov v praktických podmienkach s využitím Agdy.
⬤ Pripravuje čitateľov na pokročilejší materiál o teórii typov a dokazovaní tvrdení.
⬤ Obsahuje veľké množstvo jednoduchých dôkazov a praktických príkladov.
⬤ Vhodný pre čitateľov bez predchádzajúcich znalostí logiky alebo teórie typov, čo zvyšuje jeho dosah na publikum.

⬤ Chýba teoretické pokrytie závislých typov.
⬤ V niektorých častiach nie je kladený dôraz na veľké koncepty pred ponorením sa do detailov.
⬤ Problémy s prehľadnosťou vysvetlení a organizácie kapitol; niektoré body sa príliš opakujú, zatiaľ čo iné sú nedostatočne vysvetlené.
⬤ Verzia pre Kindle má zlé rozloženie, s nedostatočným odsadením odsekov a problémami so zarovnaním zdrojového kódu.

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