Typy spresnení: A Tutorial

Pôvodný názov:

Refinement Types: A Tutorial

Obsah knihy:

Typy spresnenia môžu byť vektorom, ktorý prinesie formálnu verifikáciu do hlavného prúdu vývoja softvéru. Tento šťastný výsledok závisí od návrhu a implementácie systémov spresňujúcich typov, ktoré sa dajú dodatočne nainštalovať do existujúcich jazykov alebo sa dajú navrhnúť spolu s novými jazykmi.

V tejto knihe autori katalyzujú vývoj takýchto systémov tým, že destilujú myšlienky rozvinuté v rozsiahlej literatúre na túto tému do koherentnej a jednotnej príručky, ktorá vysvetľuje kľúčové zložky moderných systémov spresňujúcich typov tým, že ukazuje, ako implementovať kontrolór spresňujúcich typov.

Inšpirovaní rámcom nanopasce na výučbu kompilácie autori ukazujú, ako implementovať spresňujúce typy prostredníctvom postupnosti jazykov, ktoré postupne pridávajú vlastnosti jazyka alebo typového systému.

Ľahko prístupná kniha poskytuje čitateľovi zasvätený úvod do spresňujúcich typov pomocou inovatívneho výukového štýlu, ktorý umožňuje rýchle učenie. Okrem toho sprievodná softvérová implementácia umožňuje čitateľom pracovať na praktických príkladoch z reálneho sveta.