Спецификация и формальная верификация чисто функциональных структур данных в Coq
Продолжаем писать о результатах практики в прошлом семестре. Студенты 2 курса программы «Математика, алгоритмы и анализ данных», Дмитрий Михайловский и Владимир Гладштейн, рассказывают о своём проекте. Авторский стиль в тексте сохранён без правок.
В этом проекте мы реализовали и доказали корректность работы некоторых чисто функциональных структур данных в специальном функциональном языке Coq. Теперь ими можно будет пользоваться в Coq для других доказательств и экстрагировать в Haskell или Ocaml для использования с гарантированной корректностью.
Сейчас немногие выбирают темы, связанные с функциональным программированием, и мы очень рады, что нам предоставили такую возможность. Ментором проекта стал Антон Трунов: он работает в компании Zilliqa и читает лекции по формальной верификации.
О задаче
Мы написали проект на языке Coq, интерактивном программном средстве доказательства теорем. Coq использует собственный язык функционального программирования — Gallina. Принцип работы основан на соответствии Карри-Говарда. На этом языке можно записывать и интерактивно проверять математические теоремы. Например, написать сортировку и доказать, что она действительно сортирует.
Сейчас для языка Coq нет одной большой и доступной для всех библиотеки, которая бы поддерживала различные структуры данных (кучи, деревья и т.д.). С другой стороны, большинство функциональных структур описал К. Окасаки в книге «Purely functional data structures». Мы решили, вдохновляясь книгой, восполнить этот пробел.
Реализованные структуры данных можно будет использовать внутри Coq, например, для верификации сложных алгоритмов, или снаружи: есть инструмент, который позволяет перевести код из Coq в OCaml или Haskell. Главное преимущество таких структур заключается в гарантии того, что они работают правильно.
В этом семестре мы, скорее, заложили основу: действительно быстрые и эффективные структуры мы собираемся реализовать на основе этих только в будущем. На данный момент мы реализовали бинарные деревья, левацкие и биномиальные кучи.
Доказательство терминируемости простого алгоритма
Сейчас мы приведем пример доказательства простого факта в Coq. Coq — «тотальный» язык. Это значит, что для написания алгоритма, терминируемость которого для Coq неочевидна, потребуется доказать, что он действительно остановится за конечное число шагов. Посмотрим сначала на определение кучи в Coq’e:
На двух кучах можно определить операцию их слияния “merge”. Эта операция строит по двум кучам одну, она является их объединением.
Рассмотрим теперь алгоритм, который на вход получает кучу и выдаёт список следующим образом: на каждом шаге рекурсии добавляет элемент из головы кучи в конец списка и вызывается рекуррентно на слиянии двух её подкуч.
Понятно, что количество элементов в слиянии куч равно сумме количеств элементов в двух кучах, которые мы сливаем. А, значит, размер кучи, на которой мы рекуррентно вызываемся, уменьшается на один с каждым шагом рекурсии. То есть мы сделаем ровно столько шагов рекурсии, каков размер кучи изначально, что и доказывает терминируемость алгоритма. Посмотрим на реализацию этого факта в Coq’e:
В этом случае Coq не понимает, что алгоритм останавливается, и просит доказать следующий факт:
То есть что размер кучи, который равен сумме размеров поддеревьев плюс один, действительно меньше размера кучи на след шаге рекурсии. Так это выглядит в самом Coq’e:
В этом интерфейсе то, что нужно доказать, написано справа под чертой — мы называем это «цель». Слева написаны сами доказательства и прочий код.
Для доказательства будем использовать лемму, которая гласит, что размер слияния куч — это сумма их размеров:
Тогда у нас появляется возможность воспользоваться этой леммой с помощью специальной команды “rewrite”:
Стоит обратить внимание на то, как изменилась цель после дописывания слева снизу новой команды “rewrite merge_size”: вместо размера слияния куч у нас теперь сумма их размеров.
А то, что осталось — очевидная арифметика. Такое в Coq решается специальной командой “ssrnatlia”.
И самое приятное — завершение доказательства :)
mCoq
Программы, верифицированные с помощью Coq, часто могут быть более надёжными, чем программы, корректность которых проверяется с помощью тестирования. Однако, качество формальной верификации во многом зависит от используемых определений и спецификации этой программы: если доказанные свойства программы не полностью описывают её, то недостатки определений могут остаться незамеченными. Это может привести к неопределённому поведению и ошибкам в работе программы.
Для оценки полноты спецификации существует мутационное тестирование. Оно основывается на наблюдениях за малыми изменениями в определениях.
Для Coq этот инструмент называется mCoq: он меняет определения в программе, получая модифицированную программу — она называется «мутантом». Затем mCoq проверяет свойства исходной программы на мутанте.
Если все свойства выполняются для мутанта, т.е. мутант остался жив, то можно сказать, что спецификация программы является неполной, поскольку программа с описанными свойствами не единственна.
Мы использовали мутационное тестирование для проверки спецификации бинарных деревьев поиска. Сначала мы определили бинарные деревья:
А именно: дерево может быть либо пустым, либо это вершина с двумя поддеревьями. Затем мы определили предикат, определяющий бинарное дерево поиска:
То есть дерево t является бинарным деревом поиска либо если оно пусто, либо если это дерево с вершиной x и левым и правым поддеревьями l и r соответственно, которые являются деревьями поиска, и, кроме того, выполнены свойства GT x l и LT x r. Здесь “GT x l” —это свойство, которое говорит о том, что значение x больше всех значений в дереве l, а “LT x r” говорит о том, что x меньше всех значений в r.
После этого мы определили следующие операции:
- member x t, которая проверяет, что элемент x лежит в дереве t,
- insert x t, которая вставляет элемент x в дерево t,
- makelist t, которая делает по дереву t список значений в t в порядке in-order обхода.
Запустив после этого мутационное тестирование, мы получили следующий результат:
Один мутант выжил, то есть спецификация для бинарных деревьев поиска на этом шаге является неполной. Поэтому мы добавили операции удаления элементов из дерева:
- deletemin t, которая удаляет минимальный элемент из дерева поиска t,
- delete x t, которая удаляет элемент x из дерева t.
Теперь уже мы победили всех мутантов:
Это значит, что теперь мы можем быть уверенными в нашем определении дерева поиска BSTOrder!
Как была организована работа
Работать над проектом было очень приятно. У нас был общий чат с руководителем, в котором мы обсуждали вопросы по проекту или просто по жизни, назначали онлайн или офлайн встречи и тд. Свой код мы складывали в репозиторий на GitHub и оставляли ревью на почти все коммиты друг друга.