Основы формальной верификации
Санкт-Петербург, весна 2020
Описание
Описание
О чем курс
Курс рассказывает о том как писать правильные программы
и как строго доказывать, что они правильные.
О том, что значит правильные программы
мы тоже поговорим.
Рассказ построен вокруг системы интерактивного доказательства теорем Coq, теории типов, лежащей в ее основе, и применения Coq к задачам программирования.
Если же вас когда-нибудь мучали сомнения в правильности вашего (неформального) доказательства какой-нибудь леммы или теоремы, то в этом курсе мы научимся больше не сомневаться (почти), а использовать компьютер для проверки доказательств. Мы изучим несколько языков (в том числе мета-языков) и вдоволь повеселимся, доказывая всякую всячину про функциональные алгоритмы: посортируем списки и повертим деревья -- очень полезный навык для собеседований ;)
Пререквизиты к курсу
Базовое функциональное программирование
Желательно: элементы математической логики
Родственные курсы
Что почитать
- Constructive Logic от Frank Pfenning
- Programs and Proofs от Ильи Сергея
- Mathematical Components от Assia Mahboubi и Enrico Tassi
- SSReflect Cheatsheet
Что нужно иметь с собой на занятиях
Вам будет нужен компьютер с установленным Coq и средой для редактирования: CoqIDE или VsCoq (плагин для VSCode) или Proof General (мод для Emacs).
Где прочитать про установку
Как установить Coq можно найти в wiki: https://github.com/coq/coq/wiki#coq-installation. Если установка по wiki не получается, то посмотрите еще вот это описание, содержащее рецепты для Ubuntu и macOS. Если у вас Windows, то лучшим вариантом будет использование инсталлятора со страницы релизов -- инсталлятор содержит наиболее популярные библиотеки и плагины для Coq, в том числе Mathcomp.
Если вам нужна помощь с установкой, то, пожалуйста, обратитесь ко мне до первого занятия (Телеграм: AntonTrunov) -- установка может занять достаточно много времени (иногда требуется компиляция из исходников).
Версии программ/библиотек, которые нам понадобятся
- Coq версии 8.11 (текущий патч-релиз на момент написания -- 8.11.0)
- библиотека Mathcomp версии 1.10
- среда для редактирования может быть любой относительно недавней версии
Как понять, что все установилось правильно
В псевдо-IDE по вашему выбору введите
From mathcomp Require Import ssreflect.
и выполните команду сделать шаг
или проверить весь файл
. В результате может появиться много предупреждений, но не должно быть ошибки вида
Error: Unable to locate library
ssreflect with prefix mathcomp. (While searching for a .vos file.)
Запасные варианты
- JsCoq Interactive Online System -- можно запустить Coq в браузере
- ссылка на виртуальную машину с Ubuntu (логин/пароль: coq/coq)
Что студенты будут уметь после окончания курса
После успешного прохождения курса слушатель:
Владеет основами конструктивистской логики и теории типов, умеет транслировать утверждения естественного языка на язык логики высшего порядка
Имеет практический навык компьютерных доказательств с помощью Coq, в том числе знает основные эвристические приемы доказательств по индукции
Имеет представление об основных аксиомах, которые часто используют в проектах по формализации
Имеет базовый навык специфицирования и доказательства корректности функциональных алгоритмов
Умеет играть на фортепиано (если раньше уже умел)
Владеет языком доказательств SSReflect, ориентируется в библиотеке Mathcomp и понимает ее основные архитектурные решения и подходы
Умеет программировать вывод типов при помощи канонических структур и понимает особенности работы одного из алгоритмов унификации в Coq
Критерии оценивания
Оценка за курс будет в равной степени состоять из результата выполнения практических заданий в течение курса, а также двух устных экзаменов в середине и в конце курса.
Преподаватели
Список лекций
Введение в курс: формальные методы в целом, интерактивное доказательство теорем в частности. Практическая применимость. Выдающиеся проекты в области формальных методов. Основы тотального функционального программирования в Coq: синтаксис Gallina, интерактивные запросы в Coq.
Тип-произведение, тип-сумма. Основы интуиционисткой логики и ее кодирование в Coq.
Добавим тривиально ложное и тривиально истинное утверждения и рассмотрим их соответствия в функциональном программировании. Посмотрим как закодировать (пропозициональное) равенство через индексированные индуктивные типы.
Продолжим рассмотрение зависимого сопоставления с образцом: инъективность и непересекаемость конструкторов индуктивных типов, паттерн конвой
.
Моделирование кванторов всеобщности и существования в Coq.
Рекурсия и индукция. Доказательства по индукции. Язык доказательств SSReflect.
Продолжим расширять наши знания о тактиках. Рассмотрим тактики и приемы для проведения доказательств по индукции.