Рекурсивные программы будут рассматриваться на спецкурсе
в обобщенном смысле: не просто как программы,
допускающие вызов подпрограмм, а как произвольные
непрерывные функционалы на частично упорядоченном
множестве частично определенных предикатов.
Задача верификации рекурсивных программ заключается
в анализе свойств неподвижных точек этих функционалов.
Часто требуется установить свойства неподвижных точек
этих функционалов, не вычисляя явно эти неподвижные точки.
В спецкурсе будут расмотрены методы решения задач такого типа.
Верификация рекурсивных программ представляется
мне актуальным направлением по той причине, что
сейчас все большее распространение получает
сведение многих задач анализа программ к задачам вычисления
неподвижных точек непрерывных функционалов на полных
частично упорядоченных множествах.
Например задача анализа последовательных программ сводится
к проблеме построения промежуточных утверждений (предусловий,
постусловий и инвариантов циклов), которые можно строить
итеративно: задать какие-нибудь начальные приближения
и затем последовательно их улучшать. Сейчас итеративные
методы находятся только в начальной стадии развития:
см. например статью сотрудников Стэнфордского Университета
Nikolaj Bjorner, I. Anca Browne and Zohar Manna.
"Automatic Generation of Invariants and Intermediate
Assertions". Theoretical Computer Science, vol. 173(1),
pp. 49-87, February 1997.
В основном сейчас задачи анализа программ традиционно
сводятся к проблеме логического вывода но IMHO эта традиция
скоро умрет по причине чрезвычайно высокой сложности
задач логического вывода. Будущее - за итеративными
методами, суть которых - сначала построить нужный объект
(например совокупность промежуточных утверждений для
доказательства свойство последовательной программы) грубо,
а затем улучшать его итерациями до приемлемого качества.
