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

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

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



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






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


Модел. и анализ информ. систем, 2018, том 25, номер 4, страницы 358–381 (Mi mais634)  

Верификация программ

Верификация программ со взаимной рекурсией на языке Пифагор

М. С. Ушакова, А. И. Легалов

Сибирский федеральный университет, Институт космических и информационных технологий ул. Академика Киренского, 26, г. Красноярск, 660074 Россия

Аннотация: В работе рассматривается верификация программ со взаимной рекурсией для языка функционально-потокового параллельного программирования Пифагор. В языке используется модель представления программы в виде графа потока данных (информационного графа), в котором нет дополнительных управляющих связей, а присутствуют только информационные зависимости. Это позволяет упростить процесс верификации, так как не требует анализа возникающих в традиционных архитектурах дополнительных ресурсных конфликтов.
Доказательство корректности программы опирается на удаление взаимных рекурсий посредством преобразования программы. Универсальным способом удаления взаимной рекурсии произвольного количества функций является построение универсальной рекурсивной функции, которая выполняет работу всех исходных функций и принимает, кроме аргумента выполняемой функции, натуральное число, являющееся номером выполняемой функции. В ряде случаев, когда присутствует косвенная рекурсия, можно использовать более простой способ преобразования — объединение кода функций, при котором происходит объединение тел вызывающих друг друга функций.
Для преобразования произвольной рекурсии в прямую предлагается построение графа всех связанных функций и последующая трансформация данного графа путём удаления функций, не связанных с рассматриваемой, объединения косвенно рекурсивных функций и построения универсальной рекурсивной функции. Доказывается, что изменение функции на языке Пифагор при объединении кода и построении универсальной рекурсивной функции не влияет на корректность исходной программы. Приводится пример доказательства частичной корректности программы на языке Пифагор, осуществляющей синтаксический разбор простого арифметического выражения. После построения графа всех связанных функций рассматриваются два способа доказательства: с использованием объединения кода функций и с построением универсальной рекурсивной функции.

Ключевые слова: функционально-потоковое параллельное программирование, язык программирования Пифагор, корректность рекурсий, удаление взаимной рекурсии, универсальная рекурсивная функция.

Финансовая поддержка Номер гранта
Российский фонд фундаментальных исследований 17-07-00288_а
Исследование выполняется при финансовой поддержке РФФИ в рамках научного проекта № 17-07-00288.


DOI: https://doi.org/10.18255/1818-1015-2018-4-358-381

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

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

Тип публикации: Статья
УДК: 004.052.42
Поступила в редакцию: 23.03.2018

Образец цитирования: М. С. Ушакова, А. И. Легалов, “Верификация программ со взаимной рекурсией на языке Пифагор”, Модел. и анализ информ. систем, 25:4 (2018), 358–381

Цитирование в формате AMSBIB
\RBibitem{UshLeg18}
\by М.~С.~Ушакова, А.~И.~Легалов
\paper Верификация программ со взаимной рекурсией на языке Пифагор
\jour Модел. и анализ информ. систем
\yr 2018
\vol 25
\issue 4
\pages 358--381
\mathnet{http://mi.mathnet.ru/mais634}
\crossref{https://doi.org/10.18255/1818-1015-2018-4-358-381}
\elib{http://elibrary.ru/item.asp?id=35452924}


Образцы ссылок на эту страницу:
  • http://mi.mathnet.ru/mais634
  • http://mi.mathnet.ru/rus/mais/v25/i4/p358

    ОТПРАВИТЬ: 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
  • Моделирование и анализ информационных систем
    Просмотров:
    Эта страница:30
    Полный текст:13
    Литература:2

     
    Обратная связь:
     Пользовательское соглашение  Регистрация  Логотипы © Математический институт им. В. А. Стеклова РАН, 2019