Zweryfikowano programowanie funkcjonalne w Agda

Opinie czytelników

Książka jest chwalona jako przystępne wprowadzenie do typów zależnych przy użyciu Agdy, szczególnie do praktycznego dowodzenia twierdzeń. Ma jednak znaczące niedociągnięcia w zakresie przejrzystości, organizacji i prezentacji, co wpływa na jej ogólną skuteczność.

Najbardziej przystępne wprowadzenie do typów zależnych w praktyce, szczególnie dla Agdy.

Przygotowuje czytelników do bardziej zaawansowanych książek na ten temat.

(na podstawie 4 opinii czytelników)

Oryginalny tytuł:

Verified Functional Programming in Agda

Zawartość książki:

Agda to zaawansowany język programowania oparty na teorii typów. System typów Agdy jest wystarczająco ekspresyjny, aby wspierać pełną funkcjonalną weryfikację programów, w dwóch stylach.

W weryfikacji zewnętrznej piszemy czyste programy funkcjonalne, a następnie piszemy dowody ich właściwości. Dowody są oddzielnymi zewnętrznymi artefaktami, zwykle wykorzystującymi indukcję strukturalną. W weryfikacji wewnętrznej określamy właściwości programów poprzez bogate typy dla samych programów.

Często wymaga to dołączenia dowodów wewnątrz kodu, aby pokazać modułowi sprawdzania typów, że określone właściwości mają zastosowanie. Możliwość udowadniania właściwości programów w tych dwóch stylach jest głębokim dodatkiem do praktyki programowania, dając programistom możliwość zagwarantowania braku błędów, a tym samym poprawy jakości oprogramowania w większym stopniu niż było to wcześniej możliwe. Verified Functional Programming in Agda to pierwsza książka, która zapewnia systematyczną ekspozycję zewnętrznej i wewnętrznej weryfikacji w Agda, odpowiednią dla studentów studiów licencjackich informatyki.

Nie zakłada się znajomości programowania funkcyjnego ani sprawdzanych komputerowo dowodów. Książka rozpoczyna się od wprowadzenia do programowania funkcyjnego poprzez znane przykłady, takie jak boole, liczby naturalne i listy, oraz techniki weryfikacji zewnętrznej. Weryfikacja wewnętrzna jest rozważana na przykładach wektorów, drzew wyszukiwania binarnego i drzew Brauna.

Bardziej zaawansowany materiał na temat obliczeń na poziomie typu, jawnego rozumowania o zakończeniu i normalizacji przez ocenę jest również zawarty. Książka zawiera również średniej wielkości studium przypadku dotyczące kodowania i dekodowania Huffmana.