• A
  • A
  • A
  • АБB
  • АБB
  • АБB
  • А
  • А
  • А
  • А
  • А
Обычная версия сайта

Статья

Унификация программ

Захаров В. А., Новикова Т. А.
Унифицировать два алгебраических выражения и означает отыскать такую подстановку термов вместо переменных этих выражений, чтобы оба терма и имели одинаковое значение. Задачу унификации можно распространить и на программы. Унифицировать две программы и означает отыскать такие цепочки присваиваний и , для которых композиции программ и эквивалентны (т.е. вычисляют одну и ту же функцию). В данной работе в качестве эквивалентности программ рассматривается отношение логико-термальная эквивалентности, одно из наиболее слабых разрешимых отношений эквивалентности программ, аппроксимирующих отношение функциональной эквивалентности. Опираясь на алгоритм проверки логико-термальной эквивалентности программ, мы предлагаем полиномиальную по времени процедуру вычисления наиболее общего унификатора для произвольной пары последовательных императивных программ относительно логико-термальной эквивалентности.