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

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

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

2. Boyer R.S., Moore J.S., A computational logic, Academic Press, New York, 1979, 420 pp.

3. Vazou N., Seidel E.L., Jhala R., Vytiniotis D., Peyton-Jones S., “Refinement Types for Haskell”, SIGPLAN Not., 49:9 (2014), 269–282.

4. Giesl J., “Termination of nested and mutually recursive algorithms”, Journal of Automated Reasoning, 19:1 (1997), 1–29.

5. Легалов А. И., “Функциональный язык для создания архитектурно-независимых параллельных программ”, Вычислительные технологии, 10:1 (2005), 71–89

6. Кропачева М. С., Легалов А. И., “Формальная верификация программ, написанных на функционально-потоковом языке параллельного программирования”, Моделирование и анализ информационных систем, 19:5 (2012), 81–99

7. Ushakova M. S., Legalov A. I., “Automation of Formal Verification of Programs in the Pifagor Language”, Modeling and Analysis of Information Systems, 22:4 (2015), 578–589.

8. Giesl J., “Termination of nested and mutually recursive algorithms”, Journal of Automated Reasoning, 19:1 (1997), 1–29.

9. Bevers E., Lewi J., “Proving termination of (conditional) rewrite systems”, Acta Informatica, 30:6 (1993), 537–568.

10. Plumer L., Termination Proofs for Logic Programs, Lecture Notes in Artificial Intelligence, 446, 1990, 142 pp.

11. Giesl J., “Termination Analysis for Functional Programs Using Term Orderings”, International Static Analysis Symposium, LNCS, 983, 1995, 154–171.

12. Walther C., “On Proving the Termination of Algorithm by Machine”, Artificial Intelligence, 71:1 (1994), 101–157.

13. Кушниренко А. Г., Лебедев Г. В., Программирование для математиков, Наука, М., 1988, 384 с.

14. Головешкин В. А., Ульянов М. В., Теория рекурсии для программистов, Физматлит, М., 2006, 296 с.

15. Мальцев А. И., Алгоритмы и рекурсивные функции, Наука, М., 1986, 368 с.

16. Hoare C. A. R., “An axiomatic basis for computer programming”, Communications of the ACM, 10:12 (1969), 576–585.

17. Ушакова М. С., “Семантика типов данных функционально-потокового языка параллельного программирования Пифагор”, Образовательные ресурсы и технологии, 2016, № 2(14), 263–269

18. Шилов Н. В., Основы синтаксиса, семантики, трансляции и верификации программ, Издательство СО РАН, Новосибирск, 2009, 340 с.