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

Статья

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

Захаров В. А., Новикова Т. А.
Задача унификации пары подстановок θ_1 и θ_2 состоит в вычислении такой пары подстановок η' и η'', чтобы композиции θ_1 η' и θ_2 η'' были равны. По существу, задача унификации подстановок равносильна задаче решения линейных уравнений вида θ_1 X=θ_2 Y в полугруппе подстановок. Но некоторые линейные уравнения над подстановками также можно рассматривать как новые варианты задачи унификации. В этой статье мы вводим понятие двусторонней унификации как процесса преобразования одной заданной подстановки θ_1 к другой заданной подстановке θ_2 при помощи композиции, применяемой как справа, так и слева к подстановке θ_1. Иначе говоря, задача двусторонней унификации состоит в решении уравнений вида Xθ_1 Y=θ_2. Двусторонняя унификация подстановок может быть использована при решении одной из задач реорганизации (рефакторинга) программ – выделения в заданном фрагменте кода тела библиотечной процедуры с целью последующей замены выделенного участка кода на вызов этой процедуры. В статье исследован вопрос о сложности задачи двусторонней унификации подстановок. Установлено, что эта задача является NP-полной. Доказательство NP-трудности задачи двусторонней унификации проводится путем сведения к ней NP-полной задачи правильного расположения домино в прямоугольной области плоскости. В статье также сформулирована и исследована задача двусторонней унификации программ в модели программ первого порядка с отношением логико-термальной эквивалентности. Доказано, что сформулированная задача двусторонней унификации программ также является NP-полной.