Preview

Труды Института системного программирования РАН

Расширенный поиск

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

https://doi.org/10.15514/ISPRAS-2014-26(2)-11

Полный текст:

Аннотация

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

Об авторах

Т. А. Новикова
Казахстанский филиал МГУ им. М.В. Ломоносова, Астана
Казахстан


В. А. Захаров
ИСП РАН, Москва
Россия


Список литературы

1. Захаров В.А., Новикова Т.А. Применение алгебры подстановок для унификации программ // Труды Института системного программирования РАН, - 2011. - т. 21 - с. 141-166.

2. Захаров В.А., Новикова Т.А. Полиномиальный по времени алгоритм проверки логико-термальной эквивалентности программ. // Труды Института системного программирования РАН, - 2012. - т. 22 - с. 435-455.

3. Захаров В.А., Новикова Т.А. Унификация программ. // Труды Института системного программирования РАН, - 2012. - т. 23 - с. 455-476.

4. Novikova T.A., Zakharov V.A. Is it possible to unify programs? // Proceedings of the 27-th International Workshop on Unification, Epic Series. - 2013. - v. 19 - p. 35-45.

5. Baader F., Snyder W. Unification theory // In J.A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning. - 2001. - v. 1 - p. 447-533.

6. Luckham D.C., Park D.M., Paterson M.S., On formalized computer programs // Journal of Computer and System Science - 1970. - v.4, N 3. - p. 220-249.

7. Котов В.Е., Сабельфельд В.К. Теория схем программ. - М.:Наука, 1991. - 348 с.

8. Иткин В.Э. Логико-термальная эквивалентность схем программ // Кибернетика. - 1972. - N 1. - с. 5-27.

9. Сабельфельд В.К. Полиномиальная оценка сложности распознавания логико-термальной эквивалентности // ДАН СССР. - 1979. - т. 249, N 4. - с. 793-796.

10. Фаулер М. Рефакторинг. Улучшение существующего кода. - Символ-Плюс, 2008. - 432 c.

11. Komondoor R., Horwitz S. Using slicing to identify duplication in source code // Proceedings of the 8th International Symposium on Static Analysis. - Springer-Verlag, 2001. - p. 40-56.

12. Roy C. K., Cordy J. R. A survey on software clone detection research // Technical report TR 2007-541, School of Computing, Queen’s University. - 2007. - v. 115.

13. Robinson J.A. A machine-oriented logic based on the resolution principle // Journal of the ACM. 1965 - v. 12, N 1. - p. 23-41.

14. Knight K. Unification: a multidisciplinary survey // ACM Computing Surveys - 1989. - v. 21 - N 1 - p. 93-124.

15. Baxter L.D. An efficient unification algorithm // Technical Report CS-73-23, Dep. of Analysis and Comp. Sci., University of Waterloo, Ontario, Canada, 1973.

16. Paterson M.S., Wegman M.N. Linear unification // The Journal of Computer and System Science. - 1978. - v. 16, N 2 - p. 158-167.

17. Martelli A., Montanari U. An efficient unification algorithm //ACM Transactions on Program, Languages and Systems. - 1982. - v. 4, N 2 - p. 258-282.

18. Stickel E.M. A unification algorithm for associative-commutative functions // Journal of the association for Computing Machinary. - 1981. - v. 28, N 5 - p. 423-434.

19. Herold A., Sieckmann J. Unification in Abelean semigroups // Jornal of Automated Reasoning. - 1983. - p. 247-283.

20. Lincoln P., Christian J. Adventures in associative-commutative unification //Journal of Symbolic Computation. - 1989. - v.8. - p. 393 - 416.

21. Eder E. Properties of substitutions and unifications // Journal of Symbolic Computations. - v. 1. - 1985. - p. 31-46.

22. Lewis C.H. Complexity of solvable cases of the decision problem for predicate calculus // Proceedings of the 19-th Annual Symposium on Foundations of Computer Science - 1978 - p. 35-47.

23. Zakharov V.A. On the decidability of the equivalence problem for orthogonal sequential programs // Grammars. - 2000. - v. 2 - N 3. - p. 271-281.

24. Wang Hao. Proving theorems by pattern recognition // Bell System Technical Journal. - 1961. - v. 40. - N 1. - p. 1-41.

25. Berger R. The undecidability of domino problem // Memoirs of American Mathematical Society - v. 66.

26. Lewis C.H., Papadimitriou C.H. Elements of the Theory of Computation - Prentice Hall, Englewood Cliffs, 1981.

27. Itkin V.E., Zwinogrodski Z. On program schemata equivalence // Journal of Computer and System Science. - 1972. - v.6. - N 1. - p. 88-101.

28. Zakharov V.A., Novikova T.A. Primininie algebry podstanovok dlya unifikacii program [On the application of substitution algebra to program unification]. Trudy ISP RAN [The Proceedings of ISP RAS], 2011, vol. 21, p. 141-166 [in Russian].

29. Zakharov V.A., Novikova T.A. Polynomialniy po vremeni algoritm proverki logiko-termalnoy ekvivalentnosti program [Polynomial time algorithm for checking strong equivalence of program]. Trudy ISP RAN [The Proceedings of ISP RAS], 2012, vol. 22, p. 435-455 [in Russian].

30. Zakharov V.A., Novikova T.A. Unifikaciya program [Program unification]. Trudy ISP RAN [The Proceedings of ISP RAS], 2012, vol. 23, p. 455-476 [in Russian].

31. Novikova T.A., Zakharov V.A. Is it possible to unify programs? // Proceedings of the 27-th International Workshop on Unification, Epic Series. - 2013. - v. 19 - p. 35-45.

32. Baader F., Snyder W. Unification theory. In J.A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, 2001, v. 1, p. 447-533.

33. Luckham D.C., Park D.M., Paterson M.S. On formalized computer programs // Journal of Computer and System Science. 1970, vol. 4, N 3, p. 220-249.

34. Kotov V.E. Sabelfeld V.K. Teoriya skhem program [Theory of program schemata]. Moscow, “Nauka”, 1991, 348 p.

35. Itkin V.E. Logical-termal equivalence of program schemata. Proceedings of the International Sympoisum on Theoretical Programming, 1972, p. 127-143.

36. Sabelfeld V.K. The Logic-Termal Equivalence is Polynomial-Time Decidable. Information Processing Letters, 1980, vol. 10, N 2, p. 57-62.

37. Fauler M. Refactoring: Improving the design of existing code. 1999, Addison Wesley.

38. Komondoor R., Horwitz S. Using slicing to identify duplication in source code // Proceedings of the 8th International Symposium on Static Analysis. Springer-Verlag, 2001, p. 40-56.

39. Roy C. K., Cordy J. R. A survey on software clone detection research. Technical report TR 2007-541, School of Computing, Queen’s University, 2007, vol. 115.

40. Robinson J.A. A machine-oriented logic based on the resolution principle. Journal of the ACM, 1965, vol. 12, N 1, p. 23-41.

41. Knight K. Unification: a multidisciplinary survey. ACM Computing Surveys. 1989, vol. 21, N 1, p. 93-124.

42. Baxter L.D. An efficient unification algorithm. Technical Report CS-73-23, Dep. of Analysis and Comp. Sci., University of Waterloo, Ontario, Canada, 1973.

43. Paterson M.S., Wegman M.N. Linear unification. The Journal of Computer and System Science. 1978, vol. 16, N 2, p. 158-167.

44. Martelli A., Montanari U. An efficient unification algorithm. ACM Transactions on Program, Languages and Systems. 1982, vol. 4, N 2, p. 258-282.

45. Stickel E.M. A unification algorithm for associative-commutative functions. Journal of the association for Computing Machinary. 1981, v. 28, N 5, p. 423-434.

46. Herold A., Sieckmann J. Unification in Abelean semigroups. Journal of Automated Reasoning. 1983, p. 247-283.

47. Lincoln P., Christian J. Adventures in associative-commutative unification. Journal of Symbolic Computation. 1989, vol. 8, p. 393-416.

48. Eder E. Properties of substitutions and unifications. Journal of Symbolic Computations. vol. 1, 1985, p. 31-46.

49. Lewis C.H. Complexity of solvable cases of the decision problem for predicate calculus. Proceedings of the 19-th Annual Symposium on Foundations of Computer Science, 1978, p. 35-47.

50. Zakharov V.A. On the decidability of the equivalence problem for orthogonal sequential programs. Grammars. 2000, vol. 2, N 3, p. 271-281.

51. Wang Hao. Proving theorems by pattern recognition. Bell System Technical Journal. 1961, vol. 40, N 1, p. 1-41.

52. Berger R. The undecidability of domino problem. Memoirs of American Mathematical Society, v. 66.

53. Lewis C.H., Papadimitriou C.H. Elements of the Theory of Computation - Prentice Hall, Englewood Cliffs, 1981.

54. Itkin V.E., Zwinogrodski Z. On program schemata equivalence. Journal of Computer and System Science. 1972, vol. 6, N 1, p. 88-101.


Для цитирования:


Новикова Т.А., Захаров В.А. Двусторонняя унификация программ и ее применение для задач рефакторинга. Труды Института системного программирования РАН. 2014;26(2):245-268. https://doi.org/10.15514/ISPRAS-2014-26(2)-11

Просмотров: 23


Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


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