Czy istnieją adnotowane formalne systemy weryfikacji dla czysto funkcjonalnych języków programowania?

ACSL (Ansi C Specification Language), to specyfikacja kodu C, opatrzona specjalnymi komentarzami, która pozwala na formalną weryfikację kodu C.

Nie przyjrzałem się temu, ale wyobrażam sobie, że metody formalne stosowane w weryfikatorach ACSL byłyby podobne do Hoare Logic. Jednak w przypadku czysto funkcjonalnych języków, takich jak Haskell, nie mogę sobie wyobrazić, jakiego rodzaju formalizmu można użyć do formalnej weryfikacji.

Czy ktoś stworzył coś podobnego do ACSL , ale dla czysto funkcjonalnego języka? Jeśli nie, to czy przeprowadzono badania formalnej weryfikacji stylów opatrzonych specyfikacją dla języków funkcjonalnych?

Wiem, że istnieje pisanie zależne, które obsługuje wiele języków (Agda, Idris itp.), Ale w Haskell pisanie zależne jest trudne bez wykonywania niektórych (nieczytelnych?) Kreacji. Mając to na uwadze, a ponieważ Haskell ma o wiele lepsze wsparcie bibliotek niż Agda i Idris, uważam, że taki system funkcjonalnej weryfikacji formalnej może być przydatny, ale nie wiem, czy przeprowadzono badania nad tym, czy nie.

Honda i Yoshida's

• Logika programu kompozycyjnego dla polimorficznych funkcji wyższego rzędu

(prawdopodobnie) był pionierem logiki Hoare'a dla języków wyłącznie funkcjonalnych. Praca ta oparta jest na logice Hennessy-Milnera i kodowaniu funkcji Milnera w procesach, jak opisano tutaj:

• Od logiki procesu do logiki programu

Praca Régis-Gianas i wsp., O której mowa w innej odpowiedzi, jest podobna do pierwszej pracy powyżej przedstawionej przez Honda / Yoshida. Zostało to rozszerzone na skuteczne języki w stylu ML:

• Obserwacyjnie kompletna logika programu dla imperatywnych funkcji wyższego rzędu

• Logiczna analiza aliasowania w imperatywnych funkcjach wyższego rzędu

• Logiczne uzasadnienie funkcji wyższego rzędu w stanie lokalnym

• Logika programu dla sekwencyjnej kontroli wyższego rzędu

• Logika programu dla homogenicznego meta-programowania

Wspomniane układy logiczne są nazywane kompletnie obserwacyjnie, co oznacza, że ​​semantyka operacyjna i logiczna pokrywają się. Arthur Charguéraud wykorzystał to uzupełnienie do swojej pracy nad weryfikacją programów funkcjonalnych w stylu Hoare'a w Coq.

$F^*$ , który oferuje podobne konstrukty.

Wydaje się, że istnieje ścisła zgodność między typami zawężania a notacjami typu ACSL.

Wreszcie mogę jedynie zasugerować przyjrzenie się Agdzie i Idrisowi, ponieważ mogą one kompilować się do Haskell i mają na celu zapewnienie użytkownikowi użytecznego języka programowania (zwłaszcza Idris). Podejrzewam, że bez problemu można zintegrować biblioteki Haskell z kodem Idris.

Zobacz także pracę doktorską Yanna Régisa-Gianasa z François Pottier: Logika Hoare'a dla programów funkcjonalnych Call-by-Value (MPC'08) . Prace te zostały rozszerzone, aby objąć zwykłe skutki uboczne ML przez Johannesa Kaniga i Jean-Cristophe Filliatre w 2009 r .: Who: A Verifier for Effective Higher-Programs Programs .

Jest papier w tegorocznym ICFP , rozszerzających typy dla Haskell . Artykuł dotyczy sprawdzania zakończenia, a nie pełnej logiki Hoare, ale mam nadzieję, że to początek w tym kierunku.

Powiązana sekcja pracy w tym dokumencie zawiera pewne wskazówki, takie jak Xu, Peyton-Jones i statyczne sprawdzanie kontraktu Claessena dla Haskell i Sonnex, Drossopoulou oraz Zeno i Vytiniotis Eisenbacha , Peyton-Jones, Claessen i Halo Rosen .

Nasza praca nad miękką weryfikacją umów jest powiązana na OOPSLA 2012 i OOPSLA ICFP 2014 , pozwala ci pisać umowy, które są bardzo podobne do specyfikacji ACSL, a następnie albo weryfikować je statycznie, albo używać ich do kontroli dynamicznej w czasie wykonywania.