Знакомство с формальными методами с помощью изучения системы интерактивных доказательств Coq

  • Маратович Евгений Макаров Институт информационных технологий, математики и механики; Национальный исследовательский Нижегородский государственный университет им. Н.И. Лобачевского http://orcid.org/0000-0003-0399-0946

Аннотация

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


Цели курса включают в себя углублении навыков составления строгих математических доказательств и применении знаний, полученных в ранее изучаемой дисциплины «Математическая логика». Система Coq используется в курсе для спецификации, реализации и верификации алгоритмов. В первой части курса рассматриваются темы, известные студентам, такие как арифметика и доказательства по индукции, однако на гораздо более высоком уровне строгости. Последние три-четыре недели отводятся на работу над групповым проектом, который состоит в полной спецификации и верификации алгоритма, такого как поиск максимума в одномерном и двумерном массиве, проверка числа на простоту или нахождение целочисленного корня уравнения.


В связи с тем, что курс не является профильным, а его продолжительностью ограничена, он разработан так, чтобы минимизировать нетривиальные аспекты Coq и максимально использовать знакомый студентам материал. Например, избегается использование сложных индуктивных типов и предикатов. Массивы моделируются не списками, а функциями на натуральных числах. Соответствие Карри-Говарда, на котором основана теория Coq, можно рассказывать, если позволяет время. Эта сравнительная простота, подходящая для первого знакомства с формальными методами, отличает курс от его аналогов.

Сведения об авторе

Маратович Евгений Макаров, Институт информационных технологий, математики и механики; Национальный исследовательский Нижегородский государственный университет им. Н.И. Лобачевского

Ph.D., старший преподаватель, кафедре алгебры, геометрии и дискретной математики

Опубликована
2019-12-23
Как цитировать
МАКАРОВ, Маратович Евгений. Знакомство с формальными методами с помощью изучения системы интерактивных доказательств Coq. Международный научный журнал «Современные информационные технологии и ИТ-образование», [S.l.], v. 15, n. 4, p. 871-879, dec. 2019. ISSN 2411-1473. Доступно на: <http://sitito.cs.msu.ru/index.php/SITITO/article/view/597>. Дата доступа: 27 feb. 2020 doi: https://doi.org/10.25559/SITITO.15.201904.871-879.
Раздел
Научное программное обеспечение в образовании и науке