ИСТИНА

При построении крупных программных комплексов важную роль играет ясность и простота программного кода, решающего те или иные задачи. Запутанный код с неясной структурой оказывается более дорогостоящим с точки зрения его поддержки и дальнейшего развития. Поэтому важной становится задача проверки того, может ли код быть упрощен без потери присущего ему функционала. Для решения подобного рода задач был разработан особого вида инструментарий, получивший название автоматического рефакторинга. Одним из методов рефакторинга является выделение (изъятие) программных клонов, призванное устранить дублирующиеся фрагменты кода программы и заменить их вызовами соответствующих процедур. Будучи правильно организованным, такое преобразование кода позволит во-первых повысить эффективность выполнения программы, а во-вторых — упростить ее понимание и, соответственно, сократить затраты на дальнейшую поддержку кода. В докладе рассматривается задача проверки двусторонней унифицируемости программ, которая может быть описана следующим образом. Рассмотрим две программы: P и P’. Существуют ли две программы lp1 и lp2, такие, что а) обе программы lp1 и lp2 линейны, то есть не имеют никаких операторов ветвления; б) программа, представляющая собой последовательное выполнение программ lp1; P’; lp2; , эквивалентна программе P ? Проверку того, могут ли для заданных программ P и P’ построены программы lp1 и lp2 с описанными выше свойствами, назовем задачей проверки двусторонней унифицируемости программ P и P’. Отметим, что задача проверки двусторонней унифицируемости программ непосредственно связана с задачей выделения метода: в случае, если указанные подпрограммы lp1 и lp2 существуют, программа P может быть рассмотрена как фрагмент кода, который может быть заменен вызовом процедуры P’ с соблюдением контекста состояний переменных посредством программ lp1 и lp2. Однако при решении данных задач возникает серьезная проблема. Как было показано Д. Лакхэмом, Д. Парком и М. Патерсоном, а также независимо от них А.А. Летичевским, функциональная эквивалентность программ не является алгоритмически разрешимой. В данной докладе будет рассмотрена модель стандартных схем последовательных императивных программ, введенная Патерсоном и детально изученная А.П. Ершовым. Для этой модели рассматривается логико-термальная эквивалентность, введенная В. Э. Иткиным в 1972 году. Логико-термальная эквивалентность корректна, то есть аппроксимирует функциональную эквивалентность программ, при этом является разрешимой за полиномиальное время. Полученные в результате проведенного исследования результаты оказались следующими. Задача проверки двусторонней логико-термальной унифицируемости программ является NP-полной. Для обоснования этого результата использовалось сведение известной NP-полной задачи покрытия прямоугольной области костяшками домино к задаче проверки двусторонней унифицируемости программ.