Формальная верификация программ — это набор парадигм, техник и инструментов, гарантирующих с той или иной степенью надёжности корректность программ. Думаю многие согласятся, что есть области ИТ, в которых корректность заслуживает самого пристального внимания: прошивки бортовых компьютеров самолетов, автомобилей, кардиостимуляторов, софт атомных электростанций и др.
Формальная верификация — это большая область, которую невозможно покрыть в одном курсе сколько-нибудь глубоко, поэтому нашей целью будет система интерактивного доказательства теорем Coq (https://coq.inria.fr), теория типов, лежащей в ее основе, метапрограммирование в Coq и применение Coq к верификации функциональных алгоритмов.
Лекции будут читаться через zoom. Ссылка для подключения будет опубликована в новостях курса (её получат те, кто запишется на курс).
По мере прохождения курса материалы будут выкладываться в репозитории по адресу: https://github.com/anton-trunov/csclub-coq-course-spring-2021.
парная, сильная. Эвристики для доказательств по индукции. Списки. Структурная индукция для списков.
Пожалуйста, обратите внимание, что программа курса примерная и перечень тем, а также глубина их рассмотрения может корректироваться по ходу курса.
Телеграм: https://t.me/joinchat/Ge1_yrqEFxEzYjAy. В чате можно попросить помощи с инсталляцией (см. ниже), что-то уточнить, обсудить домашние задания, указать на ошибки/опечатки и т.п.
Вам будет нужен компьютер со следующим установленным программным обеспечением
Важно: без интерактивной среды взаимодействие с Coq сильно усложняется. Если вы очень не любите среды для редактирования, то можно использовать интерпретатор coqtop
, входящий в комплект поставки Coq.
В настоящий момент рекомендуемый способ установить Coq на Linux и Windows -- это воспользоваться Coq Platform, помимо Coq включающей в себя большое количество предустановленных библиотек. Про этот способ установки можно прочитать в wiki: https://github.com/coq/coq/wiki#coq-installation.
Если вам нужна помощь с установкой, то, пожалуйста, обратитесь в чат курса до первого занятия (Телеграм: https://t.me/joinchat/Ge1_yrqEFxEzYjAy) -- установка может занять достаточно много времени (иногда требуется компиляция из исходников).
В интерактивной среде по вашему выбору введите
From mathcomp Require Import ssreflect.
и выполните команду сделать шаг
или проверить весь файл
. В результате может появиться много предупреждений, но не должно быть ошибки вида
Error: Unable to locate library
ssreflect with prefix mathcomp. (While searching for a .vos file.)