Formalna semantyka OCaml w Coq

14

Semantyka dużego podzbioru OCaml, zwanego OCamllight , została sformalizowana w HOL przez Owensa kilka lat temu. Niedawno Kreitz, Hayden i Hickey zaimplementowali w Nuprl teoretyczną semantykę typu mniejszego podzbioru OCaml .

Czy istnieje podobny rozwój w Coq?

coq program-verification ocaml Andrea Asperti
źródło
Możesz być zainteresowany CakeML: cakeml.org . Jednak nie jestem specjalnie OCaml.
jmite

Odpowiedzi:

12

Czy widziałeś pracę doktorską Arthura Charguérauda, Charakterystyczne formuły weryfikacji programu zmechanizowanego ?

Zamiast budować system typów i semantykę małych kroków jako relacje indukcyjne, podaje technikę przekształcania programów Camla w charakterystyczne formuły. Jest to w zasadzie uogólnienie semantyki transformatora predykatowego w celu obsługi bardzo dużego podzbioru Ocaml - w tym w szczególności niebezpiecznych rzutów Obj.magic. Cytując z pracy magisterskiej:

Skoncentrowałem się na podzbiorze języka programowania OCaml, który jest sekwencyjnym językiem programowania wysokiego poziomu o wartości „call-by-value”. Obecna implementacja CFML obsługuje podstawowy rachunek λ, w tym funkcje wyższego rzędu, rekurencję, wzajemną rekurencję i rekurencję polimorficzną. Obsługuje krotki, konstruktory danych, dopasowanie wzorców, komórki referencyjne, rekordy i tablice. Zapewniam dodatkową bibliotekę Caml, która dodaje obsługę zerowych wskaźników i silne aktualizacje.

Jest to bardzo atrakcyjne podejście, jeśli chcesz udowodnić poprawność konkretnego programu Caml (mniej, jeśli interesuje Cię jego metateoria).

Neel Krishnaswami
źródło
Tak więc, jeśli dobrze rozumiem, specyfikacja semantyki Ocaml jest osadzona w systemie. Czy można interpretować charakterystyczną formułę (jakiejś kluczowej funkcji) systemu jako taką specyfikację? Zakładam też, że system jest napisany w OCaml. Czy można określić i udowodnić jego poprawność w samym systemie?
Andrea Asperti
Dla danego programu OCaml jego charakterystyczną formułę można uznać za denotacyjną semantykę, „najmniej ogólną” specyfikację, której można użyć do udowodnienia dowolnych pożądanych właściwości programu. Jeśli mówisz o „poprawności” samego CFML, pytanie brzmi: w odniesieniu do jakiej alternatywnej semantyki formalnej?
gasche
Dziwne jest mieć program, który ma certyfikować oprogramowanie i którego zachowania nie można określić :)
Andrea Asperti
@AndreaAsperti Co rozumiesz przez „osadzony w systemie”? Idea charakterystycznych formuł (CF) jest dość prosta: mapuj programy na formuły logiczne (zwykle przed i po warunkach), takie formuły dokładnie opisują semantykę programów. Innymi słowy, dwa programy spełniają te same współczynniki CF, jeśli są kontekstowo nierozróżnialne. Mapowanie od programu do CF odbywa się poprzez indukcję struktury programu i może być ukierunkowane na dowolną wystarczająco ekspresyjną logikę. A. Logika celownika Charguérauda, ​​ale jest to warunkowy wybór.
Martin Berger,
1
@MartinBerger: artykuł Guéneau i in. Udowadnia jedynie solidność, ponieważ pochodne post / post nie charakteryzują programów, z których pochodzą. Ich CF pochodzą z nietypowej semantyki CakeML, ale język maszynowy ma inną równoważną obserwację. (Dla praktycznej weryfikacji nie jest to strasznie ważne i jest łatwiejsze.)
Neel Krishnaswami,
8

Możesz być zainteresowany Certyfikowaną implementacją ML Jacka Garrigue'a z polimorfizmem strukturalnym i typami rekurencyjnymi , która określa solidność statycznej i dynamicznej semantyki oraz wnioskowanie o typie dla języka ML z (rekurencyjnym i) strukturalnym polimorfizmem, formalizując w ten sposób jeden z bardziej zaawansowane rogi OCaml (warianty polimorficzne i typy obiektów).

To powiedziawszy, ta praca jest bardziej ukierunkowana na sprawdzenie poprawności bardziej zaawansowanych części systemu typów niż na omówienie zestawu funkcji istniejących programów OCaml. Myślę, że jeśli chodzi o próbę udowodnienia poprawności istniejącego programu OCaml, CFML byłby lepszym wyborem.

gasche
źródło