Formalna semantyka OCaml w Coq

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

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,

@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,

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