Введение к работе
Актуальность темы. Программы, создаваемые программистом вручную или, чаще, с использованием разнообразных систем автоматизации программирования, обычно подлежат многократному улучшению посредством их эквивалентного преобразования, — чтобы удовлетворить предъявляемые к этим программам требования надежности и эффективности. Преобразование называют эквивалентным, если оно переводит исходную программу в такую программу, которая реализует ту же самую функцию. Говорят, что система преобразований полна для некоторого класса программ, если применением ее правил можно переводить друг в друга всякие эквивалентные программы. Эквивалентные преобразования получают широкое распространение в связи с развитием трансформационного подхода к программированию, при котором весь процесс решения задачи на ЭВМ представляет собой систематическое применение преобразований, начиная от неалгоритмической спецификации высокого уровня и кончая эффективной программой решения задачи.
Как следует из теоремы Раиса, содержательные отношения эквивалентности в классе программ, вычисляющих все рекурсивные функции, не являются рекурсивно перечислимыми, так что полную систему преобразований таких программ построить в принципе невозможно. Поэтому от программ переходят к их моделям — схемам, в которых абстрагируются от некоторых особенностей программ. Лля схем вводят отношение эквивалентности и строят эквивалентные преобразования схем. Моделируя программу схемой, по построенному эквивалентному преобразованию схемы мы получаем эквивалентные преобразования всех программ, моделируемых данной схемой. Полная система преобразований схем привлекательна тем, что она содержит исчерпывающий набор эквивалентных преобразований схем. . О том, что мы понимаем какое-то отношение эквивалентности или о том, что отношение эквивалентности полностью изучено, можно говорить только тогда, когда для этого отношения удалось построить полную систему эквивалентных преобразований и, по возможности, эффективную процедуру распознавания эквивалентности. Этот тезис содержит в себе одну из главных причин поиска полных систем преобразований для отношений эквивалентности. Проблема построе-
ния полной теории для широкого класса схем программ и для достаточно слабого отношения эквивалентности, — теории, в которой был бы объединен анализ управляющих связей, сделанный для схем Янова, с анализом информационных связей, сделанным для схем Лаврова, была названа А.П. Ершовым фундаментальной проблемой теории программирования.
Основы теории схем программ, центральной задачей которой является проблема эквивалентных преобразований, были заложены в работах А.А. Ляпунова, Ю.И. Янова, А.П. Ершова, В.М. Глушкова, А.А. Летичевского, Д. Лахэма, Д. Парка и М. Патерсона. Значительный вклад в развитие теории внесли Ф.Е. Аллен, М. Берд, Дж. Маккарти, С. Игараши, Н.А. Криницкий, С. Гарлэнд, Дж. Бэкус, 3. Манна, Д. Скотт, В.В. Мартынюк, С.С. Лавров, В.А. Тузов, Г.А. Килдел, Р.И. Под-ловченко, Дж. деБаккер, Б.К. Розен, Э. Ашкрофт, А. Пнуели, Дж. Кок, В.А. Непомнящий, В.Э. Иткин, А.О. Буда, Дж. Кэм, Дж.Д. Ульман, Б. Курсель, П. Кузо и Р. Кузо, А.В. Анисимов, Л.П. Лисовик, В.Н. Касьянов, В.Е. Котов, А.Б. Годлевский, Г.Н. Петросян, С.Л. Кривой, и другие.
Несмотря на достигнутые успехи, полного завершения теория эквивалентных-преобразований не получила. Общезначимые полные системы преобразований были построены фактически только для функциональной эквивалентности схем Янова (Ю.И.Янов 1958,1968, А.П.Ершов 1967) и для введенной В.Э.Иткиным логико-термальной эквивалентности стандартных схем (В.К.Сабельфельд 1979). Для моделей рекурсивных программ систематического исследования эквивалентных преобразований не проводилось вовсе.
Цель работы состояла в построении математических основ эквивалентных преобразований для моделей императивных и рекурсивных программ, в выявлении свойств программ, существенных для преобразований, в построении алгоритмов обнаружения таких свойств.
Методы исследований. В работе использованы математические методы исследования из теории конечных автоматов, теории алгоритмов и рекурсивных функций, из теории сложности алгоритмов и вычислений, из теории аксиоматических
систем.
Научная и практическая ценность. Научная ценность работы определяется тем, что в ней получены новые математические результаты в решении проблемы эквивалентных преобразований для моделей императивных и функциональных программ.
Практическая ценность результатов диссертации заключается в возможности их использования при построении новых систем автоматизации программирования, в том числе трансляторов, оптимизаторов и анализаторов программ.
Научная новизна. В работе предлагается новое направление в теории схем программ — теория эквивалентных преобразований схем программ на основе анализа содержательных свойств. Эквивалентные преобразования в этой теории основаны на анализе семантических свойств тех вычислений, что описываются схемой программ. Задачами этого нового направления являются
выявление таких содержательных свойств программ и схем программ, знание которых позволяет производить эквивалентные преобразования;
построение математических основ, методов и алгоритмов для распознавания содержательных свойств программ;
построение полных систем преобразований для различных моделей программ и отношений эквивалентности на основе анализа содержательных свойств;.
разработка программных инструментов, облегчающих отладку программ, на основе алгоритмов анализа содержательных свойств программ.
Публикации и апробация. Основные результаты работы докладывались на Всесоюзной конференции по методам трансляции (Новосибирск, 1981), на Всесоюзном семинаре "Оптимизация и преобразование программ" (Новосибирск, 1982), на национальной школе болгарских Математиков по программирова-
нию (Приморско, 1983), на Всесоюзном семинаре "Алгоритмические проблемы в программировании" (Цесис, 1984), на конференции ИФИП по спецификации и преобразованиям программ (Бад-Тельц, 1986), на Всесоюзной конференции "Проблемы совершенствования синтеза, тестирования и отладки программ" (Рига, 1986), на советско-французском семинаре "Информатика 88" (Ницца,1988), на советско-французском симпозиуме "Информатика 91" (Гренобль,1991), на Всесоюзной конференции по прикладной логике (Новосибирск, 1988), на международной конференции по формальным методам в программировании и приложениях (Новосибирск, 1993), а также на научных семинарах Института систем информатики и Вычислительного центра СО РАН (Новосибирск), Института кибернетики им. В.М. Глушко-ва АН Украины (Киев), Дрезденского технического университета, Института информатики Мюнхенского технического университета, Института математики Аугсбургского университета, лаборатории теоретической информатики и программирования университета Париж-7. Основные результаты работы отражены в 40 публикациях.
Структура и объем работы. Диссертация состоит из введения, четырех глав, заключения и списка цитируемой литературы, насчитывающего 141 наименований. Объем работы 251 стр., включая 18 рисунков.
