Сборники трудов ИСП РАН


Полиномиальный по времени алгоритм проверки логико-термальной эквивалентности программ.

В.А.Захаров, Т.А. Новикова.

Аннотация

Логико-термальная эквивалентность программ – это одно из наиболее слабых отношений эквивалентности программ, аппроксимирующих отношение функциональной эквивалентности и обладающих разрешающим алгоритмом. В данной статье предложена новая модификация алгоритма проверки логико-термальной эквивалентности программ, основанная на операции вычисления точной нижней грани в решетке конечных подстановок. Показано, что трудоемкость предложенного алгоритма оценивается величиной O(n6) , где n - размер анализируемых программ.

Полученная верхняя оценка сложности задачи проверки логико-термальной эквивалентности программ существенно меньше ранее известных полиномиальных оценок сложности указанной задачи.

Ключевые слова

программа, логико-термальная эквивалентность программ, подстановка, антиунификация, сложность

Издание

Труды Института системного программирования РАН, том 22, 2012, стр.435-455.

ISSN 2220-6426 (Online), ISSN 2079-8156 (Print).

DOI: 10.15514/ISPRAS-2012-22-23

Полный текст статьи в формате pdf Вернуться к содержанию тома