Jakie są popularne formalne techniki potwierdzania poprawności kodu funkcjonalnego?

Chcę przedstawić dowody dla części programu Haskell, który piszę w ramach mojej pracy magisterskiej. Jednak jak dotąd nie udało mi się znaleźć dobrej pracy referencyjnej.

Książka wprowadzająca Grahama Huttona Programowanie w Haskell ( Google Books ) - którą czytam podczas nauki Haskell - porusza kilka technik rozumowania programów, takich jak

• rozumowanie równań
• za pomocą nienakładających się wzorów
• indukcja listy

w rozdziale 13, ale nie jest to zbyt szczegółowe.

Czy są jakieś książki lub artykuły, które możesz polecić, które zawierają bardziej szczegółowy przegląd formalnych technik sprawdzania kodu Haskell lub innego funkcjonalnego kodu?

Jedną z faktycznych metod potwierdzania wyników w programowaniu funkcjonalnym jest grupa Richarda Birda.

W szczególności prosisz o dogłębne lub przynajmniej bardziej kompleksowe podejście do wnioskowania równań i indukcji listy, co zostało przedstawione w Wykładach o konstruktywnym programowaniu funkcjonalnym .

Mówiąc bardziej ogólnie, tekst „Algebra programowania” autorstwa Bird i de Moor dotyczy również poprawności algorytmów funkcjonalnych, takich jak problemy z optymalizacją i programowaniem dynamicznym.

Jeśli natrafisz na inne przydatne zasoby dotyczące tego problemu, proszę o nich wspomnieć, a być może możemy zamienić ten post w wiki.

Możesz zacząć od

• Software Foundations autorstwa Benjamina C. Pierce i in.

Tematy obejmują podstawowe pojęcia z zakresu logiki, komputerowego dowodzenia twierdzeń, asystenta dowodu Coq, programowania funkcjonalnego, semantyki operacyjnej, logiki Hoare'a i systemów typu statycznego. Ekspozycja przeznaczona jest dla szerokiego grona czytelników, od zaawansowanych studentów, doktorantów i badaczy. Nie zakłada się żadnego szczególnego tła w językach logiki lub programowania, choć pomocny będzie pewien stopień dojrzałości matematycznej.

Możesz pominąć (lub przejrzeć) części teorii języka programowania i nauczyć się, jak radzić sobie z formalnymi dowodami, poczynając od Wstępu aż po IndPrinciples. Książka jest naprawdę dobrze napisana i pouczająca.

Następnie możesz kontynuować

• Zweryfikowane algorytmy funkcjonalne Andrew W. Appela

W tym tomie nauczysz się określać i weryfikować (potwierdzać poprawność) algorytmy sortowania, drzewa wyszukiwania binarnego, zrównoważone drzewa wyszukiwania binarnego i kolejki priorytetowe. Przed skorzystaniem z tej książki powinieneś trochę zrozumieć te algorytmy i struktury danych, dostępne w każdym standardowym podręczniku do algorytmów licencjackich. Powinieneś zrozumieć cały materiał z Software Foundations Volume 1 (Logic Foundation)

Uwaga: VFA jest wciąż w wersji beta!

Okazuje się, że doskonałym źródłem technik dowodowych i przykładów do udowodnienia rzeczy o czysto funkcjonalnych językach są asystenci dowodowi, którzy zwykle zawierają jako część swojego języka specyfikacji czysty język funkcjonalny, w którym możliwe jest racjonalne uzasadnienie.

Ktoś może chcieć zajrzeć do książki takiej jak Certyfikowane programowanie z typami zależnymi, aby uzyskać szczegółowe wprowadzenie do tego rodzaju rozumowania w konkretnym asystencie dowodowym, a mianowicie Coq.

Sugeruję użycie logiki programu. Radzą sobie znacznie lepiej z efektami niż systemy pisania.

Istnieje wiele logiki programów dla języków funkcjonalnych. Staje się to interesujące z efektami. Patrz np. Logiczne uzasadnienie funkcji wyższego rzędu w stanie lokalnym .

Praca Arthura Charguérauda integruje logikę programu z asystentami dowodowymi, patrz np. Ta strona przeglądu .