Формальная семантика OCaml в Coq

14

Семантика большого подмножества OCaml, называемого OCamllight , была формализована в HOL Оуэнсом несколько лет назад. Совсем недавно теоретическая семантика типов меньшего подмножества OCaml была реализована в Nuprl Крейцем, Хейденом и Хикки .

Есть ли похожие разработки в Coq?

coq program-verification ocaml Андреа Асперти
источник
Вас может заинтересовать CakeML: cakeml.org . Я не OCaml конкретно, хотя.
19

Ответы:

12

Вы видели кандидатскую диссертацию Артура Шерго, « Характеристические формулы для механизированной верификации программ» ?

Вместо того, чтобы строить систему типов и семантику малых шагов как индуктивные отношения, он дает метод для преобразования программ Caml в характеристические формулы. Это в основном обобщение семантики предикатного преобразователя для поддержки очень большого подмножества Ocaml - особенно, включая небезопасные приведения типа Obj.magic. Цитирую его тезис:

Я сосредоточился на подмножестве языка программирования OCaml, который представляет собой последовательный язык программирования высокого уровня с вызовом по значению. Текущая реализация CFML поддерживает ядро ​​λ-исчисления, включая функции высшего порядка, рекурсию, взаимную рекурсию и полиморфную рекурсию. Он поддерживает кортежи, конструкторы данных, сопоставление с образцом, ссылочные ячейки, записи и массивы. Я предоставляю дополнительную библиотеку Caml, которая добавляет поддержку нулевых указателей и сильных обновлений.

Это очень привлекательный подход, если вы хотите доказать правильность конкретной программы Caml (тем не менее, если вы заинтересованы в ее метатеории).

Нил Кришнасвами
источник
Итак, если я правильно понял, спецификация семантики Ocaml встроена в систему. Можно ли интерпретировать характеристическую формулу (некоторую ключевую функцию) системы как такую ​​спецификацию? Также я предполагаю, что система написана на OCaml. Можно ли указать и доказать его правильность в самой системе?
Андреа Асперти
Для данной программы OCaml ее характерная формула может рассматриваться как денотационная семантика, «наименее общая» спецификация, которую можно использовать для доказательства любых желательных свойств программы. Если вы говорите о «правильности» самого CFML, возникает вопрос: в отношении какой альтернативной формальной семантики?
Гаше
Странно иметь программу, которая должна сертифицировать программное обеспечение и чье поведение не может быть определено :)
Андреа Асперти
@AndreaAsperti Что вы подразумеваете под «встроенным в систему»? Идея, лежащая в основе характерных формул (CF), довольно проста: сопоставить программы с логическими формулами (обычно до и после условия), такими формулами, которые точно описывают семантику программ. Другими словами, две программы удовлетворяют одним и тем же CF, если они не различаются по контексту. Отображение из программы в CF осуществляется путем наведения структуры программы и может быть нацелено на любую достаточно выразительную логику. Логика цели Царя Шарго, но это случайный выбор.
Мартин Бергер
1
@MartinBerger: статья Гено и др. Только подтверждает правильность, потому что производные пре / посты не характеризуют программы, из которых они получены. Их CF получены из нетипизированной семантики CakeML, но типизированный язык имеет другую наблюдательную эквивалентность. (Для практической проверки это не очень важно, и это проще.)
Нил Кришнасвами,
8

Вас может заинтересовать « Сертифицированная реализация ML со структурным полиморфизмом и рекурсивными типами» Жака Гаррига , которая устанавливает надежность статической и динамической семантики и свойства вывода типов для языка ML со (рекурсивным и) структурным полиморфизмом, таким образом формализуя один из более продвинутые углы OCaml (полиморфные варианты и типы объектов).

Тем не менее, эта работа больше направлена ​​на проверку правильности более продвинутых частей системы типов, чем на рассмотрение набора функций существующих программ OCaml. Я думаю, что с точки зрения попытки доказать правильность существующей программы OCaml, CFML был бы лучшим выбором.

gasche
источник