Сборники трудов ИСП РАН


Верификация преобразования грамматики в нормальную форму Хомского в F*

М.И. Полубелова (СПбГУ, Санкт-Петербург, Россия)
С.Н. Божко (СПбГУ, Санкт-Петербург, Россия)
С.В. Григорьев (СПбГУ, Санкт-Петербург, Россия)

Аннотация

Сертификационное программирование позволяет доказывать, что программа соответствует своему формальному описанию. Проверка корректности производится статически, благодаря чему становится возможным отказаться от дальнейшего тестирования проверифицированных программ. Среди инструментов, предназначенных для сертификационного программирования, только инструмент F* позволяет реализовывать программы на языке общего назначения и автоматизирует доказательство их корректности. Последнее означает, что инструмент F* автоматически выведет доказательство корректности, где это возможно, при этом пользователь может специфицировать более сложные доказательства, если это необходимо. Мы работаем над применением данного подхода к проекту YaccConstructor ‒ платформе для исследования и разработки генераторов лексических и синтаксических анализаторов и других алгоритмов для работы с грамматиками. В данной статье рассматривается верификация реализации одного из таких алгоритмов  ‒  преобразования грамматики в нормальную форму Хомского ‒ что является первой задачей на пути к верификации всего проекта YaccConstructor. Для программы, реализующей данное преобразование, доказаны завершаемость и тотальность, а также установлен порядок применения используемых в ней основных преобразований с использованием зависимых и уточняющих типов. Следующим важным направлением данной работы является доказательство эквивалентности исходной и преобразованной грамматик. Инструмент F* позволяет извлекать код, написанный на F*, как программу на языке программирования F# или OCaml. Так как F# является основным языком разработки проекта YaccConstructor, это позволит сохранить совместимость проверифицированных программ с существующими в проекте. В статье сформулированы преимущества и недостатки применения инструмента F*.

Ключевые слова

сертификационное программирование; F*; верификация программ; контекстно-свободная грамматика; нормальная форма Хомского; преобразование грамматики; dependent type; refinement type

Издание

Труды Института системного программирования РАН, том 28, вып. 2, 2016, стр. 127-138.

ISSN 2220-6426 (Online), ISSN 2079-8156 (Print).

DOI: 10.15514/ISPRAS-2016-28(2)-8

Полный текст статьи в формате pdf (на английском) Вернуться к содержанию тома