Введение
1 Алгоритмы антиунификации подстановок 14
1.1 Подстановки и их представление 14
1.1.1 Подстановки, решетка подстановок 15
1.1.2 Графовые представления подстановок 18
1.2 Слолсность задачи антиунификации в классе последовательных ал горитмов 20
1.2.1 Алгоритм редукции 20
1.2.2 Алгоритм антиунификации для подстановок, представленных ациклическими ориентированными графами 23
1.2.3 Нижняя оценка сложности задачи антиунификации подстановок 28
1.3 Параллельные алгоритмы 32
1.3.1 Алгоритм распознавания точного антиунификатора 32
1.3.2 Алгоритм построения точного антиунификатора 41
1.4 Вычисление инвариантов равенства программ с использованием ан тиунификации подстановок 46
1.4.1 Модель одномодульной программы 46
1.4.2 Инварианты равенства одномодульных программ и методы их вычисления 50
2 Обобщенные подстановки 56
2.1 Метаконтексты и метаподстановки 57
2.1.1 Понятия контекста и метаконтекста 57
2.1.2 Решетка метаконтекстов 64
2.1.3 Метаподстановки и их основные алгебраические свойства . 83
2.1.4 Операция конкретизации метаподстановок 105
2.2 Антиунификация для метаподстановок 121
2.2.1 Представление метаконтекстов конечными автоматами . 121
2.2.2 Алгоритм антиунификации метаконтекстов 129
3 Инварианты многомодульных программ 141
3.1 Многомодульные программы и инварианты равенства 142
3.1.1 Модель многомодульной программы 142
3.1.2 Инварианты равенства программ и их представление мета-подстановками 148
3.1.3 Аппроксимирующие последовательности 155
3.2 Вычисление инвариантов равенства программ при помощи метапод становок 164
3.2.1 Построение аппроксимирующей последовательности 164
3.2.2 Алгоритм построения инвариантов равенства 167
Заключение 170
Литература 173
Приложение 177
