О чем курс

В круг тем, охватываемых данным предметом, входят подходы к точному описанию семантики языковых конструкций и методам доказательства корректности преобразований программ.

• Операционная семантика малого и большого шага императивного языка программирования,

• Денотационная семантика,

• Аксиоматическая семантика Хоара,

• Семантика языков с многопоточностью,

• Слабые модели памяти.

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

Функциональное программирование

Желательно: Математическая логика

Что студенты будут уметь после окончания курса

После успешного прохождения курса слушатель:

• Знает основные стили семантик языков программирования: денотационный, операционный, аксиоматический; композиционность. Умеет аргументированно описать выбранный стиль и преимущества его использования для конкретной задачи.

• Знает эквивалентность программ и семантик. Знает варианты определений и их взаимоотношения, обоснование свойств преобразований программ.

• Знает понятие операционной семантики. Умеет получать и анализировать дерево вывода программы. Владеет навыками использования семантики большого и малого шагов.

• Обладает базовыми навыками работы с системой интерактивного доказательства теорем Coq. Умеет формализовывать различные семантики и доказательства их свойств в Coq, а также верифицировать программы с помощью логики Хоара.

Критерии оценивания

Оценка за курс будет в равной степени состоять из результата выполнения практических заданий в течение курса, а также двух устных экзаменов в середине и в конце курса.

Максимум за курс 10 баллов:

• 4 балла за домашние задания (на языке Coq);

• 2 балла за устный экзамен №1;

• 2 балла за устный экзамен №2;

• 2 балла за активность на занятиях.

Что нужно иметь с собой на занятиях

Будет нужен компьютер с установленным Coq и средой для редактирования (см. ниже).

Установка Coq и нужных библиотек

С помощью opam нужно установить библиотеки coq>=8.14.0 и hahn. Заметим, что на момент прочтения этого курса библиотека hahn несовместима с последними версиями coq, поэтому надо явно задать ограничение сверху на версию пакета:

opam remote add coq-released https://coq.inria.fr/opam/released
opam remote add coq-weakmemory-local -k git https://github.com/weakmemory/local-coq-opam-archive
opam install "coq<8.15.0" coq-hahn

Также можно зафиксировать необходимую версию coq, чтобы при обновлении пакетов случайно не обновить coq до несовместимой версии:

opam pin add coq 8.14.1

Среда для редактирования Coq

Coq предполагает интерактивное взаимодействие, поэтому понадобится или специальный редактор (CoqIDE), или плагин для вашего любимого текстового редактора (ProofGeneral для Emacs, VsCoq для VSCode). Для Vim тоже есть, но рекомендовать не могу -- использовал давно.

Мы используем Emacs (+ Evil mode для эмуляции Vim в Emacs).

Виртуальная машина

Виртуальная машина (Ubuntu 18) с установленным Coq 8.14.0, необходимыми библиотеками и IDE доступна здесь. Логин/пароль vagrant.

Практические задания

Вводные задания по Coq расположены здесь, задания по семантикам - здесь.

Литература

• Glynn Winskel. The Formal Semantics of Programming Languages;
• Coq tactics cheatsheets (краткая информация по тактикам): Link 1, Link 2
• Полная информация по тактикам: Coq Reference Manual;
• Классический вводный курс по Coq: Software Foundations. Logical Foundations.

Родственные курсы

• Основы формальной верификации

На нашем курсе про Coq будет рассказан необходимый минимум для задачек, которые будут рассматриваться на семинаре, и Coq будет в первую очередь инструментом для доказательства свойств семантик. Курс Основы формальной верификации предлагает более подробный рассказ про Coq.