Лялямбда

школа верификации, компиляторов и реверса

'21

с элементами прикладного ФП

17-07—01/08

Формальная верификация Интро

Владимир Гладштейн и Антон Трунов

Формальная верификация программ — это набор парадигм, техник и инструментов, гарантирующих с той или иной степенью надёжности корректность программ. Думаю, многие согласятся, что есть области ИТ, в которых корректность заслуживает самого пристального внимания: прошивки бортовых компьютеров самолетов, автомобилей, кардиостимуляторов, софт атомных электростанций и др.

Формальная верификация — это большая область, которую невозможно покрыть в одном курсе сколько-нибудь глубоко, поэтому нашей целью будет система интерактивного доказательства теорем Coq (https://coq.inria.fr), теория типов, лежащей в ее основе, метапрограммирование в Coq и применение Coq к верификации (простых) компиляторов.

Пререквизиты к курсу

Примерная программа курса

  1. Введение в курс, основы тотального функционального программирования в Coq, интерактивные запросы в Coq.
  2. Алгебраические типы данных, элементы соответствия Карри-Говарда, интуиционистская логика высказываний.
  3. Кванторы всеобщности и существования. Доказательства по индукции.
  4. Язык тактик SSReflect. Эвристики для доказательств по индукции. Списки. Структурная индукция для списков.
  5. Типы с равенством (eqType). Плагины Equations, QuickChick. Рандомизированное тестирование свойств.
  6. Верификация серии простых компиляторов из арифметических выражений в несколько вариаций стековой машины.

Программа примерная: перечень тем и глубина рассмотрения будут корректироваться по ходу курса.

Полезные ссылки

Программное обеспечение для семинаров/практических занятий

Вам будет нужен компьютер со следующим установленным программным обеспечением

Важно: без интерактивной среды взаимодействие с Coq сильно усложняется. Если вы очень не любите среды для редактирования, то можно использовать интерпретатор coqtop, входящий в комплект поставки Coq.

Где прочитать про установку

В настоящий момент рекомендуемый способ установить Coq на Linux и Windows – это воспользоваться Coq Platform, помимо Coq включающей в себя большое количество предустановленных библиотек. Про этот способ установки можно прочитать в wiki: https://github.com/coq/coq/wiki#coq-installation.

Если вам нужна помощь с установкой, то, пожалуйста, обратитесь в чат курса до первого занятия – установка может занять достаточно много времени (иногда требуется компиляция из исходников).

Если вы поставили пакетный менеджер opam, установили компилятор OCaml, то выполните следующие команды:

opam switch create coq8.13 4.11.1
opam repo add coq-released https://coq.inria.fr/opam/released
opam pin add coq 8.13.2 --no-action
opam pin add coq-mathcomp-ssreflect 1.12.0 --no-action
opam install coq coq-mathcomp-ssreflect coq-mathcomp-zify coq-equations coq-quickchick coq-deriving

Как понять, что все установилось правильно

Настройте путь до coqtop для вашей интерактивной среды (редактора), введите

From Equations Require Import Equations.
From QuickChick Require Import QuickChick.
Import GenLow GenHigh.
From deriving Require Import deriving.
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
From mathcomp Require Import zify.

и выполните команду “проверить весь файл”. В результате может появиться много предупреждений, но не должно быть ошибки вида

Error: Unable to locate library
<название библиотеки> with prefix <префикс>. (While searching for a .vos file.)

Запасные варианты