|
Computing methodologies and applications
Комплексный подход системы C-lightVer к автоматизированной локализации ошибок в C-программах
Д. А. Кондратьев, А. В. Промский Институт систем информатики им. А. П. Ершова СО РАН,
пр. Академика Лаврентьева, 6, г. Новосибирск, 630090 Россия
Аннотация:
В ИСИ СО РАН разрабатывается система C-lightVer для дедуктивной верификации С-программ. Исходя из двухуровневой архитектуры системы, входной язык C-light транслируется в промежуточный язык C-kernel. Метагенератор условий корректности принимает на вход C-kernel программу и логику Хоара для C-kernel. Для решения известной проблемы задания инвариантов циклов выбран подход финитных итераций. Тело цикла финитной итерации исполняется один раз для каждого элемента структуры данных конечной размерности, а правило вывода для них использует операцию замены rep, выражающую действие цикла в символической форме. Также в нашем метагенераторе внедрен и расширен метод семантической разметки условий корректности. Он позволяет порождать пояснения для недоказанных условий и упрощает локализацию ошибок. Наконец, если система ACL2 не справляется с установлением истинности условия, можно сосредоточиться на доказательстве его ложности. Ранее нами был разработан способ доказательства ложности условий корректности для системы ACL2. Необходимость в более подробных объяснениях условий корректности, содержащих операцию замены rep, привела к изменению алгоритмов генерации операции замены, извлечения семантических меток и генерации объяснений недоказанных условий корректности. В статье представлены модификации данных алгоритмов. Эти изменения позволяют пометить исходный код функции rep семантическими метками, извлекать семантические метки из определения rep, а также генерировать описание условия исполнения инструкции break.
Ключевые слова:
дедуктивная верификация, семантическая метка, локализация ошибок, C-lightVer, ACL2, метагенератор условий корректности, финитная итерация, стратегия доказательства.
Поступила в редакцию: 23.09.2019 Исправленный вариант: 25.11.2019 Принята в печать: 27.11.2019
Образец цитирования:
Д. А. Кондратьев, А. В. Промский, “Комплексный подход системы C-lightVer к автоматизированной локализации ошибок в C-программах”, Модел. и анализ информ. систем, 26:4 (2019), 502–519
Образцы ссылок на эту страницу:
https://www.mathnet.ru/rus/mais694 https://www.mathnet.ru/rus/mais/v26/i4/p502
|
Статистика просмотров: |
Страница аннотации: | 71 | PDF полного текста: | 68 | Список литературы: | 24 |
|