RUS  ENG ЖУРНАЛЫ   ПЕРСОНАЛИИ   ОРГАНИЗАЦИИ   КОНФЕРЕНЦИИ   СЕМИНАРЫ   ВИДЕОТЕКА   ПАКЕТ AMSBIB
Общая информация
Последний выпуск
Архив
Импакт-фактор

Поиск публикаций
Поиск ссылок

RSS
Последний выпуск
Текущие выпуски
Архивные выпуски
Что такое RSS



Модел. и анализ информ. систем:
Год:
Том:
Выпуск:
Страница:
Найти






Персональный вход:
Логин:
Пароль:
Запомнить пароль
Войти
Забыли пароль?
Регистрация


Модел. и анализ информ. систем, 2015, том 22, номер 6, страницы 773–782 (Mi mais473)  

Loop invariants elimination for definite iterations over unchangeable data structures in C programs

[Элиминация инвариантов циклов для финитной итерации над неизменяемыми структурами данных в Си программах]

I. V. Maryasov, V. A. Nepomniaschy

A.P. Ershov Institute of Informatics Systems SB RAS, Akademik Lavrentiev pr., 6, Novosibirsk, 630090, Russia

Аннотация: Верификация С-программ является актуальной проблемой современного программирования. Для применения известных методов дедуктивной верификации необходимо аннотировать циклы посредством инвариантов, что во многих случаях является трудной задачей. В этой статье мы рассматриваем язык C-light, который является выразительным подмножеством языка C, соответствующего стандарту ISO. Для верификации C-light программ нами были предложены двухуровневый подход [19,20] и метод смешанной аксиоматической семантики [1,3,11]. На первой стадии этого подхода исходная C-light программа транслируется [17] в программу на языке C-kernel [19], который является подмножеством языка C-light. Теорема о корректности этой трансляции была доказана в [10,11]. По сравнению с C-light в языке C-kernel меньше операторов, что позволяет уменьшить число правил вывода при разработке аксиоматической семантики. На второй стадии этого подхода для программ на языке C-kernel порождаются условия корректности по правилам смешанной аксиоматической семантики [10,11], которая может содержать несколько правил вывода для одной и той же программной конструкции. В таких случаях правила вывода применяются однозначно в зависимости от контекста. Заметим, что во многих случаях использование смешанной аксиоматической семантики позволяет упростить условия корректности. В этой статье представлено расширение данного подхода, которое включает наш метод верификации для финитной итерации над неизменяемыми структурами данных без выхода из тела цикла в C-light программах. Данный метод содержит новое правило вывода для таких финитных итераций без инвариантов. Это правило было реализовано в генераторе условий корректности. На стадии доказательства используется SMT-решатель Z3 [12]. Рассмотрен пример, иллюстрирующий применение данного подхода.
Статья представляет собой расширенную версию доклада на VI Международном семинаре “Program Semantics, Specification and Verification: Theory and Applications”, Казань, 2015.
Статья публикуется в авторской редакции.

Ключевые слова: Си, инварианты циклов, смешанная аксиоматическая семантика, финитная итерация, неизменяемые структуры данных, спецификация, верификация, логика Хоара.

Финансовая поддержка Номер гранта
Российский фонд фундаментальных исследований 15-01-05974
Эта работа выполнена при поддержке гранта РФФИ 15-01-05974.


DOI: https://doi.org/10.18255/1818-1015-2015-6-773-782

Полный текст: PDF файл (482 kB)
Список литературы: PDF файл   HTML файл

Реферативные базы данных:

Тип публикации: Статья
УДК: 519.681.3
Поступила в редакцию: 26.10.2015
Язык публикации: английский

Образец цитирования: I. V. Maryasov, V. A. Nepomniaschy, “Loop invariants elimination for definite iterations over unchangeable data structures in C programs”, Модел. и анализ информ. систем, 22:6 (2015), 773–782

Цитирование в формате AMSBIB
\RBibitem{MarNep15}
\by I.~V.~Maryasov, V.~A.~Nepomniaschy
\paper Loop invariants elimination for definite iterations over unchangeable data structures in C programs
\jour Модел. и анализ информ. систем
\yr 2015
\vol 22
\issue 6
\pages 773--782
\mathnet{http://mi.mathnet.ru/mais473}
\crossref{https://doi.org/10.18255/1818-1015-2015-6-773-782}
\mathscinet{http://www.ams.org/mathscinet-getitem?mr=3493710}
\elib{http://elibrary.ru/item.asp?id=25125094}


Образцы ссылок на эту страницу:
  • http://mi.mathnet.ru/mais473
  • http://mi.mathnet.ru/rus/mais/v22/i6/p773

    ОТПРАВИТЬ: VKontakte.ru FaceBook Twitter Mail.ru Livejournal Memori.ru


    Citing articles on Google Scholar: Russian citations, English citations
    Related articles on Google Scholar: Russian articles, English articles
  • Моделирование и анализ информационных систем
    Просмотров:
    Эта страница:110
    Полный текст:54
    Литература:26
     
    Обратная связь:
     Пользовательское соглашение  Регистрация  Логотипы © Математический институт им. В. А. Стеклова РАН, 2020