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

Санкт-Петербург, весна 2020

Описание

Описание

О чем курс

Курс рассказывает о том как писать правильные программы и как строго доказывать, что они правильные. О том, что значит правильные программы мы тоже поговорим. Рассказ построен вокруг системы интерактивного доказательства теорем Coq, теории типов, лежащей в ее основе, и применения Coq к задачам программирования.

Если же вас когда-нибудь мучали сомнения в правильности вашего (неформального) доказательства какой-нибудь леммы или теоремы, то в этом курсе мы научимся больше не сомневаться (почти), а использовать компьютер для проверки доказательств. Мы изучим несколько языков (в том числе мета-языков) и вдоволь повеселимся, доказывая всякую всячину про функциональные алгоритмы: посортируем списки и повертим деревья -- очень полезный навык для собеседований ;)

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

  • Базовое функциональное программирование

  • Желательно: элементы математической логики

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

Что почитать

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

Вам будет нужен компьютер с установленным 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.)

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

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

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

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

  • Имеет практический навык компьютерных доказательств с помощью Coq, в том числе знает основные эвристические приемы доказательств по индукции

  • Имеет представление об основных аксиомах, которые часто используют в проектах по формализации

  • Имеет базовый навык специфицирования и доказательства корректности функциональных алгоритмов

  • Умеет играть на фортепиано (если раньше уже умел)

  • Владеет языком доказательств SSReflect, ориентируется в библиотеке Mathcomp и понимает ее основные архитектурные решения и подходы

  • Умеет программировать вывод типов при помощи канонических структур и понимает особенности работы одного из алгоритмов унификации в Coq

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

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

Преподаватели

Список лекций

Введение в курс, основы функционального программирования в Coq

Введение в курс: формальные методы в целом, интерактивное доказательство теорем в частности. Практическая применимость. Выдающиеся проекты в области формальных методов. Основы тотального функционального программирования в Coq: синтаксис Gallina, интерактивные запросы в Coq.

Алгебраические типы данных. Интуиционистская пропозициональная логика

Тип-произведение, тип-сумма. Основы интуиционисткой логики и ее кодирование в Coq.

Интуиционистские связки (продолжение). Равенство

Добавим тривиально ложное и тривиально истинное утверждения и рассмотрим их соответствия в функциональном программировании. Посмотрим как закодировать (пропозициональное) равенство через индексированные индуктивные типы.

Равенство (продолжение). Кванторы всеобщности и существования

Продолжим рассмотрение зависимого сопоставления с образцом: инъективность и непересекаемость конструкторов индуктивных типов, паттерн конвой. Моделирование кванторов всеобщности и существования в Coq.

Индукция и рекурсия. Язык доказательств SSReflect

Рекурсия и индукция. Доказательства по индукции. Язык доказательств SSReflect.

Доказательства по индукции в SSReflect

Продолжим расширять наши знания о тактиках. Рассмотрим тактики и приемы для проведения доказательств по индукции.