Информационная система "Конференции"

Тезисы докладов

Информационные технологии

Формальная верификация программ - актуальное направление современного программирования. В лаборатории теоретического программирования ИСИ СО РАН разрабатывается система верификации программ, ориентированная на поддержку нескольких языков программирования, включая Паксаль, С и их расширения. Эта система состоит из следующих основных компонент: входной анализатор, генератор условий корректности и их доказатель. В данной работе рассматривается генерация условий корректности для языков Паскаль и C-light [2,3], которая для программ над массивами использует метод элиминации инвариантов циклов [1].

Формальным базисом для генерации условий корректности (УК) является аксиоматическая семантика языка программирования, также известная как логика Хоара. Элиминируя программные конструкции, эта система вывода позволяет получить набор лемм о свойствах программы - условия корректности.

В работе представлены следующие теоретические результаты. Во-первых, классическая система Хоара для языка Паскаль была расширена семантикой указателей и методом элиминации инвариантов циклов для программ над массивами. Во-вторых, была получена аксиоматическая семантика языка C-light, который является представительным подмножеством языка С. Корректность этих сементик гарантируется доказанными теоремами непротиворечивости. Также для каждого языка была создана эквивалентная модифицированная система обратного просмотра, благодаря чему процесс вывода становится детерминированным.

Практическим результатом стало создание генераторов УК для этих языков. Каждый генератор состоит из следующих частей: 1) входной синтаксический анализатор, обрабатывающий аннотированную программу в независимом лиспоподобном представлении и определяющий порядок генерации для отдельных блоков исходной программы; 2) рекурсивная процедура генерации, реализующая вывод УК; 3) интерфейс пользователя, позволяющий определить дальнейшую обработку полученных УК. Генераторы УК поддерживают механизм локализации ошибок, обнаруживаемых на этапе доказательства УК. Языком реализации является SML, средства определения типов которого являются весьма удобными для данной задачи. В качестве тестов задавались программы сортировки, линейной алгебры, работы с файлами и указателями.

Работа частично поддержана грантом РФФИ 00-01-00909.

1. Непомнящий А. В., Рякин О.М. Прикладные методы верификации программ. // М.: Радио и связь, 1988. - 256 с.

2. Непомнящий В.А., Ануреев И.С., Михайлов И.Н., Промский А.В. На пути к верификации С программ. Часть 2. Язык C-light-kernel и его аксиоматическая семантика. --- Новосибирск, 2001. --- (препр. / РАН. Сиб. Отд-ние. ИСИ; N 87).

3. Непомнящий В.А., Ануреев И.С., Михайлов И.Н., Промский А.В. На пути к верификации С программ. Язык C-light и его формальная семантика. // Программирование, 2002, N 6, c. 1-13.

Примечание. Тезисы докладов публикуются в авторской редакции

Ваши комментарии Обратная связь

[Головная страница] [Конференции]

© 1996-2000, Институт вычислительных технологий СО РАН, Новосибирск
© 1996-2000, Сибирское отделение Российской академии наук, Новосибирск
    Дата последней модификации: 06-Jul-2012 (11:47:01)