Алгоритмы антиунификации и их применение для вычисления инвариантов программ

• Автор: Костылев, Егор Вячеславович
• Шифр специальности: 01.01.09
• Научная степень: Кандидатская
• Год защиты: 2008
• Место защиты: Москва
• Количество страниц: 220 с.

Оглавление
Введение

1 Алгоритмы антиунификации подстановок

1.1 Подстановки и их представление

1.1.1 Подстановки, решетка подстановок

1.1.2 Графовые представления подстановок

1.2 Сложность задачи антиунификации в классе последовательных алгоритмов

1.2.1 Алгоритм редукции

1.2.2 Алгоритм антиунификации для подстановок, представленных

ациклическими ориентированными графами

1.2.3 Нижняя оценка сложности задачи антиуннфикации подстановок

1.3 Параллельные алгоритмы
1.3.1 Алгоритм распознавания точного антиунификатора
1.3.2 Алгоритм построения точного антиунификатора
1.4 Вычисление инвариантов равенства программ с использованием антиунификации подстановок
1.4.1 Модель одномодульной программы
1.4.2 Инварианты равенства одномодульных программ и методы
их вычисления

ОГЛАВЛЕНИЕ
2 Обобщенные подстановки
2.1 Метаконтексты и метаподстановки
2.1.1 Понятия контекста и метаконтекста
2.1.2 Решетка метаконтекстов
2.1.3 Метаподстановки и их основные алгебраические свойства
2.1.4 Операция конкретизации метаподстановок
2.2 Антиунификация для метаподстановок
2.2.1 Представление метаконтекстов конечными автоматами
2.2.2 Алгоритм антиунификации метаконтекстов
3 Инварианты многомодульных программ
3.1 Многомодульные программы и инварианты равенства
3.1.1 Модель многомодульной программы
3.1.2 Инварианты равенства программ и их представление метаподстановками
3.1.3 Аппроксимирующие последовательности
3.2 Вычисление инвариантов равенства программ при помощи метаподстановок
3.2.1 Построение аппроксимирующей последовательности
3.2.2 Алгоритм построения инвариантов равенства
Заключение
Литература
Приложение

Введение
Задача антиунификации (англ. anti-unification, generalization) была впервые рассмотрена в работах [18] и [20]. В общем виде она состоит в том, чтобы для двух заданных выражений Е и Е2 отыскать наиболее специальное выражение Е0, примерами которого являются оба выражения Ei и Е2, то есть существуют подстановки $! и i52, для которых выполняются равенства Ei = E06>i и Е2 = Е0т!>2- Такое выражение Ео называется наименее общим шаблоном выражений Е и Е2.
Задача антиунификации двойственна гораздо более широко исследованной задаче унификации. Последняя состоит в том, чтобы для двух заданных выражений Ei и Е2 отыскать наиболее общее выражение Е0, которое является примером обоих выражений Ei и Ео, то есть удовлетворяет равенствам Ец — -Ецгд и Е0 = Е2г]2 для некоторых подстановок г)i и щ. Такое выражение Eq называется наиболее общим примером выражений Ех и Е2. Задача унификации была впервые исследована Дж. Робинсоном [21] в 1965 году в связи с созданием метода резолюций для автоматического доказательства теорем. В дальнейшем метод резолюций послужил отправной точкой для разработки концепции логического программирования, и алгоритмы унификации фактически стали основным средством вычисления логических программ. За прошедшие годы задача унификации была детально исследована. В частности, был разработан широкий спектр эффективных алгоритмов унификации [2, 12, 17, 27, 28], имеющих почти линейную сложность, а также были найдены подходящие структуры данных для практической реализации этих алгоритмов. Одной из таких структур для представления подстановок являют-

ГЛАВА 1. АЛГОРИТМЫ АНТИУНИФИКАЦИИ ПОДСТАНОВОК
меньше, чем валентность их пометок. Для того, чтобы подчеркнуть принадлежность к остовному дереву Т, будем иногда использовать СИМВОЛЫ УтД), X € X, для обозначения вершин УдДх), х е X. Заметим, что некоторые из этих вершин могут совпадать. Обозначим символом Х-т произвольное подмножество переменных из X, такое что все вершины Ут(х), х € Х-т, различны, и для каждой переменной х' из множества ХХт существует переменная х из множества Х-т, такая что
УтД) = Доопределение 1.7. Пусть заданы множество функциональных символов Т и множества рабочих и вспомогательных переменных X и У. Пусть и - произвольные подстановки из множества ЗиЪв1[Х, У, Т, а <ЗД) и ОД}?) - представляющие их АОГ. Наложением остовного леса Т АОГ ОД1) на АОГ 0Д2) назовем отображение
и : УеНех{Т) —> УеВех{0Д2)),
такое что:
- для каждой переменной х из множества Хт верно равенство
ЩУт(х)) = УдШ(х)
- для каждой вершины V из множества УеНехЦГ) и для каждой исходящей из нее дуги (Ц V') с номером г в дереве Т верно равенство
Ю(П = *5се№)(Р(1/),г).
Заметим, что наложение остовного леса Т АОГ ЯД{) на АОГ ОДэ) существует не для любых подстановок $1 и б)2-
Определение 1.8. Пусть заданы множество функциональных символов Л и множество вспомогательных переменных У. Направленным путем Т> назовем помеченное ориентированное корневое дерево, в котором