Programare funcțională verificată în Agda

Recenzii ale cititorilor

Cartea este lăudată ca o introducere accesibilă la tipurile dependente folosind Agda, în special pentru demonstrarea teoremei practice. Cu toate acestea, are deficiențe notabile în ceea ce privește claritatea, organizarea și prezentarea, afectând eficacitatea sa generală.

Cea mai accesibilă introducere la tipurile dependente în practică, în special pentru Agda.

Pregătește cititorii pentru cărți mai avansate pe această temă.

(pe baza a 4 recenzii ale cititorilor)

Titlul original:

Verified Functional Programming in Agda

Conținutul cărții:

Agda este un limbaj de programare avansat bazat pe teoria tipurilor. Sistemul de tipuri al Agda este suficient de expresiv pentru a susține verificarea funcțională completă a programelor, în două stiluri.

În verificarea externă, scriem programe pur funcționale și apoi scriem dovezi ale proprietăților acestora. Dovezile sunt artefacte externe separate, folosind de obicei inducția structurală. În verificarea internă, specificăm proprietățile programelor prin tipuri bogate pentru programele în sine.

Acest lucru necesită adesea includerea de dovezi în interiorul codului, pentru a arăta verificatorului de tip că proprietățile specificate sunt valabile. Puterea de a dovedi proprietățile programelor în aceste două stiluri este un adaos profund la practica programării, oferind programatorilor puterea de a garanta absența erorilor și, astfel, de a îmbunătăți calitatea software-ului mai mult decât era posibil anterior. Programarea funcțională verificată în Agda este prima carte care oferă o expunere sistematică a verificării externe și interne în Agda, potrivită pentru studenții de licență de la Informatică.

Nu se presupune nicio familiaritate cu programarea funcțională sau cu probele verificate de calculator. Cartea începe cu o introducere în programarea funcțională prin exemple familiare precum booleenii, numerele naturale și listele, și tehnici de verificare externă. Verificarea internă este luată în considerare prin exemple de vectori, arbori de căutare binară și arbori Braun.

De asemenea, sunt incluse materiale mai avansate privind calculul la nivel de tip, raționamentul explicit privind terminarea și normalizarea prin evaluare. Cartea include, de asemenea, un studiu de caz de dimensiuni medii privind codarea și decodarea Huffman.