Narzędzie do prototypowania semantyki języka programowania

Czy jest jakieś narzędzie do prototypowania semantyki języka programowania i systemu typów, a także umożliwia pewnego rodzaju sprawdzanie modelu standardowych właściwości, takich jak poprawność typu?

Pytam o to, ponieważ czytam książkę o stopie i zapewnia on dokładnie taką funkcjonalność, jakiej chcę, ale dla modeli wyrażonych za pomocą logiki relacyjnej.

Zdaję sobie sprawę z Ott , ale nie ma takiej możliwości „sprawdzania modelu”, ponieważ koncentruje się na generowaniu kodu dla systemów asystenta dowodu.

Wszelkie odniesienia do takiego istnienia narzędzi byłyby fajne.

Chociaż istnieją ramy stworzone specjalnie w celu prototypowania języków programowania (w tym ich semantyki, systemów typów, oceny, a także sprawdzania ich właściwości), najlepszy wybór zależy od konkretnego przypadku i konkretnych potrzeb.

Powiedziawszy to, istnieje wiele (być może nie tak wyraźnych) alternatyw, które możesz wziąć (w tym te, o których już wspomniałeś):

• przy użyciu określonego języka / frameworka zaprojektowanego do tworzenia i prototypowania nowych języków: na przykład Redex [1], język specyficzny dla domeny osadzony w Racket do określania i sprawdzania (operacyjnej) semantyki języków programowania, co, biorąc pod uwagę definicję język, zapewnia łatwą obsługę zadań, takich jak skład tekstu (w lateksie), kontrola śladów redukcji, testy jednostkowe i testy losowe (np. do sprawdzania pisania)
• stosowanie ogólnych języków modelowania, które oferują łatwe definiowanie i przeprowadzanie niektórych analiz, o ile potrafią one uchwycić konkretny język w niezbędnym zakresie; Stop [2] jest przykładem takiego podejścia: choć dość ogólne i elastyczne, języki mogą być modelowane jako relacje między stanami, podczas gdy wsparcie sprawdzania modelu (np. Ocena w takim języku) przychodzi za darmo po wyrażeniu semantyki za pomocą model relacji (np. niektóre pomysły na modelowanie semantyki języka można znaleźć w [3])
• osadzanie języka w celu sprawdzenia jego właściwości za pomocą twierdzenia twierdzącego; przykład zdefiniowałby język oraz jego semantykę poprzez osadzenie go w systemie dowodowym, takim jak Coq [4] (więcej szczegółów na temat tego podejścia, a także omówienie i wykazanie różnicy między głębokim a płytkim osadzaniem w Coq podano w [ 5])
• korzystanie z Ott (jak już wspomniano, w duchu podobnym do Redex, ale zapewnianie nowego języka definicji zamiast osadzania); Ott umożliwia definiowanie języka programowania w wygodnej notacji oraz tworzenie składu i definicji w systemie proof (zwykle z głębokim osadzaniem), w którym większość sprawdzania (tj. Proof) należy wykonać ręcznie
• rozwijanie języka i jego semantyki, a także odpowiednie sprawdzanie (np. jako testy) „od zera” w języku programowania ogólnego i w razie potrzeby tłumaczenie na inne systemy (w niektórych językach, np. Leon [6], obejmują wbudowane weryfikatory, które pozwalają automatycznie sprawdzać pewne właściwości i upodabniają to podejście do osadzania w systemie proof)

Zauważ, że istnieje kompromis między tym, jak łatwe jest użycie frameworka / narzędzia (np. Tak proste, jak opracowanie definicji na papierze lub w lateksie), a tym, jak potężne są mechanizmy sprawdzania właściwości języka (np. Osadzanie język w twierdzeniu twierdzącym pozwala sprawdzać bardzo wyszukane właściwości).

[1] Casey Klein, John Clements, Christos Dimoulas, Carl Eastlund, Matthias Felleisen, Matthew Flatt, Jay A. McCarthy, Jon Rafkind, Sam Tobin-Hochstadt i Robert Bruce Findler. Przeprowadź badania: dotyczące skuteczności lekkiej mechanizacji. POPL, 2012.

[2] Daniel Jackson. Stop: notacja lekkiego modelowania obiektów. TOSEM, 2002.

[3] Greg Dennis, Felix Chang, Daniel Jackson. Modułowa weryfikacja kodu za pomocą SAT. ISSTA, 2006

[4] System zarządzania dowodami formalnymi Coq

[5] Formalne uzasadnienie programów. Adam Chlipala, 2016

[6] Leon automatyczny system do weryfikacji, naprawy i syntezy funkcjonalnych programów Scala