Конференции ИВТ СО РАН

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

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

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

В данной работе предложена модифицированная аксиоматическая семантика C-kernel программ, позволяющая автоматически получать условия корректности и упрощать их. Разработана система верификации C-light программ, состоящая из следующих модулей:

1. Модуль трансляции, который переводит входной текст программы на языке C-light в лиспопободную форму, удобную для дальнейшей обработки.
2. Модуль перевода из языка C-light в язык C-kernel, который осуществляет трансляцию исходной программы в программу на языке C-kernel.
3. Генератор условий корректности, который, получая на вход аннотированную программу на языке C-kernel, порождает её условия корректности.
4. Блок упрощения, применяющий различные стратегии для приведения условий корректности к более простому виду.
5. Блок доказательств, который проводит доказательство порождённых условий корректности в диалоговом режиме с пользователем. В качестве этого модуля используется система PVS.

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

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

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

© 1996-2000, Институт вычислительных технологий СО РАН, Новосибирск
© 1996-2000, Сибирское отделение Российской академии наук, Новосибирск