Как формально проверить компилятор (интерфейс и/или серверную часть)?
В проекте, который я собираюсь начать, я изучал формальную проверку компилятора. Я наткнулся на компилятор C CompCert , который является официально проверенным компилятором C, удостоенным награды ACM.
Когда я прочитал дальше, он упомянул, что использовал Coq Proof Assistant для механизации автоматической проверки.
Вопрос в том, как создать доказательства/теоремы для перевода инструкций? Каковы шаги? Любые рекомендации приветствуются .
2 ответа
Ксавье Леруа провел курс по этой теме в Коллеж де Франс в 2019/2020 году¹. Сами уроки проходят на французском языке, но отличный материал доступен на английском здесь: https://github.com/xavierleroy/cdf-mech-sem . В частности, файлыImp.vиCompil.vдаст вам отличную фору в освоении основ.
Однако прямой переход к коду Coq, вероятно, будет непростым. Посещение Фонда программного обеспечения сначала или параллельно, как отметил kiner_shah, — отличная идея.
В разработке сообщества coq существует гораздо более простой компилятор для педагогических целей, который называется семантика.
Существует также очень простой синтаксический анализатор и другие инструменты, связанные с языком, такие как инструмент для проверки программ по самому слабому предусловию и абстрактный интерпретатор (чтобы доказать, что переменные остаются в некоторых интервалах).