ПИШЕМ ПРАВИЛЬНЫЕ ПРОГРАММЫ
Премия имени академика А.П.Ершова присуждается молодым ученым за работы в
области информатики, теории и автоматизации программирования.
Победителем конкурса этого года стал кандидат физико-математических наук,
научный сотрудник Института систем информатики СО РАН Игорь
АНУРЕЕВ за цикл статей "Методы автоматического доказательства,
ориентированные на верификацию программ".
Исследования, описанные
в этом цикле статей, — составная часть проекта "СПЕКТР", который
выполняется в лаборатории теоретического программирования. Проект
посвящен разработке проблемно-ориентированной системы верификации
программ. Система предназначена для проверки правильности "C" и
"Pascal" программ. Однако применение системы не ограничено этими
двумя языками. Система позволяет добавлять новые языки
программирования в специальном формате, описывающем смысл
программных конструкций.
Доказательство правильности программы — сложная задача.
Некоторого упрощения можно достичь, разбивая ее на подзадачи.
Система СПЕКТР состоит из пяти модулей. Каждый модуль нацелен на
решение определенной подзадачи. Модуль предварительной обработки
программ переводит программу на языке программирования в
программу на внутреннем языке. Остальные модули оперируют уже
программами, заданными на этом языке. Модуль преобразования
программ преобразует программу со сложными конструкциями в более
простую. Модуль генерации теорем строит по программе и описанию
требований, которым она должна удовлетворять, математическую
теорему. Если эта теорема истинна, то программа правильна, то
есть все требования для нее выполняются. Модуль доказательства
проводит доказательство теорем, которые получены из модуля
генерации теорем. В случае, если доказать теорему не удалось,
применяется модуль анализа. Он определяет входные данные, при
которых программа работает неправильно, и места в программе, где
были допущены ошибки.
Цикл статей посвящен разработке методов автоматического
доказательства таких теорем. Описанные в нем методы позволяют
задавать аксиомы и леммы, необходимые для доказательства теорем,
также как стратегии применения этих аксиом и лемм. Доказательство
теорем, полученных для программ из конкретного класса,
характеризуется своим набором аксиом и лемм вместе со стратегиями
их применения. Этот набор составляет базу знаний для проблемной
области, описывающей данный класс программ. Можно выделить такие
проблемные области, как программы сортировки, программы линейной
алгебры, программы редактирования текстов и т. д. Каждая из них
имеет свою базу знаний, задающую средства доказательства
правильности программ из соответствующего класса. Система
верификации СПЕКТР является проблемно-ориентированной, так как
она для каждой проблемной области строит свою базу знаний.
Методы, описанные в цикле статей, позволили построить базу знаний
для ряда программ сортировки массивов и файлов, позволяющую
проводить доказательство теорем полностью автоматически и,
соответственно, автоматически доказывать правильность программ
относительно заданных требований.
Подготовила Г.Шпак.
стр.
|
