Ellenőrzött funkcionális programozás az Agda-ban

Olvasói vélemények

A könyvet dicsérik, mint az Agda segítségével elérhető bevezetést a függő típusokba, különösen a gyakorlati tételbizonyításhoz. Ugyanakkor figyelemre méltó hiányosságai vannak az áttekinthetőség, a szervezés és a bemutatás terén, ami kihat az általános hatékonyságára.

A legkönnyebben hozzáférhető bevezetés a függő típusok gyakorlati használatába, különösen az Agda esetében.

Felkészíti az olvasót a témában haladóbb könyvekre.

(4 olvasói vélemény alapján)

Eredeti címe:

Verified Functional Programming in Agda

Könyv tartalma:

Az Agda egy fejlett programozási nyelv, amely a típuselméleten alapul. Az Agda típusrendszere elég kifejező ahhoz, hogy támogassa a programok teljes funkcionális verifikációját, kétféle stílusban.

A külső verifikációban tiszta funkcionális programokat írunk, majd tulajdonságbizonyításokat írunk róluk. A bizonyítások különálló külső műtárgyak, jellemzően strukturális indukciót használva. A belső verifikációban a programok tulajdonságait maguknak a programoknak a gazdag típusain keresztül adjuk meg.

Ez gyakran szükségessé teszi a kódon belüli bizonyítások beillesztését, hogy megmutassuk a típusellenőrzőnek, hogy a megadott tulajdonságok érvényesek. A programok tulajdonságainak e két stílusban történő bizonyításának képessége mélyreható kiegészítést jelent a programozás gyakorlatában, mivel a programozóknak hatalmat ad a hibák hiányának garantálásához, és így a szoftverek minőségének a korábban lehetségesnél nagyobb mértékű javításához. A Verified Functional Programming in Agda az első olyan könyv, amely szisztematikusan mutatja be az Agda külső és belső verifikációját, és amely alkalmas az informatika alapszakos hallgatók számára.

Nem feltételezi a funkcionális programozás vagy a számítógéppel ellenőrzött bizonyítások ismeretét. A könyv a funkcionális programozás bevezetésével kezdődik, olyan ismerős példákon keresztül, mint a boolék, természetes számok és listák, valamint a külső verifikáció technikái. A belső verifikációt a vektorok, a bináris keresőfák és a Braun-fák példáin keresztül vizsgáljuk.

A típusszintű számítás, a befejezéssel kapcsolatos explicit érvelés és a kiértékeléssel történő normalizálás haladóbb anyaga is szerepel. A könyv egy közepes méretű esettanulmányt is tartalmaz a Huffman-kódolásról és -dekódolásról.