Полиномиальный по времени алгоритм проверки логико-термальной эквивалентности программ
Аннотация
Логико-термальная эквивалентность программ - это одно из наиболее слабых отношений эквивалентности программ, аппроксимирующих отношение функциональной эквивалентности и обладающих разрешающим алгоритмом. В данной статье предложена новая модификация алгоритма проверки логико-термальной эквивалентности программ, основанная на операции вычисления точной нижней грани в решетке конечных подстановок. Показано, что трудоемкость предложенного алгоритма оценивается величиной O(n6), где n - размер анализируемых программ. Полученная верхняя оценка сложности задачи проверки логико-термальной эквивалентности программ существенно меньше ранее известных полиномиальных оценок сложности указанной задачи.
Ключевые слова
Список литературы
1. Иткин В.Э. Логико-термальная эквивалентность схем программ // Кибернетика. — 1972. — N 1. — с. 5-27.
2. Сабельфельд В.К. Полиномиальная оценка сложности распознавания логико-термальной эквивалентности // ДАН СССР. — 1979. — т. 249, N 4. — с. 793-796.
3. Sabelfeld V.K. The logic-termal equivalence is polynomial-time decidable // Information Processing Letters. — 1980 — v. 10, N 2. — p. 57-62.
4. Буда А.О., Иткин В.Э. Сводимость эквивалентности программ к термальной эквивалентности // Системное и теоретическое программирование. Сборник статей. Т. 1. — Кишенев, 1974. — с. 293-324.
5. Буда А.О. Об одной модели вычислений над памятью с разрешимой проблемой эквивалентности // Доклады АН СССР — 1979. — т. 245, N 1.
6. Буда А.О. Канонизация логической структуры логико-термально эквивалентных схем программ // Трансляция и модели программ. — Новосибирск, 1980.
7. Годлевский А.Б. О связи логико-термальной эквивалентности схем программ с одним случаем специальной проблемы эквивалентности дискретных преобразователей // Кибернетика. — 1975. — N 5. — с. 32-34.
8. Хачатрян В.Е. Логико-термальная эквивалентность в классе схем над сильно невырожденным базисом // Программирование. — 1977. — N 3. — с. 20-27.
9. Сабельфельд В.К. Некоторые оптимизирующие преобразования для стандартных схем программ // Языки и системы программирования. — Новосибирск, 1979.
10. Син Мен Де. Логико-термально эквивалентные преобразования схем программ // Кибернетика. — 1976 — N 5.
11. Фаулер М. Рефакторинг. Улучшение существующего кода. — Символ-Плюс, 2008. — 432 c.
12. 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.
13. Bulychev P., Kostylev E., Zakharov V. Anti-unification algorithms and their applications in program analysis // Proceedings of the 7th International Conference “Perspectives of System Informatics”, June 15-19, 2009, Novosibirsk. — 2009. — p. 82-89.
14. 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.
15. Itkin V.E., Zwinogrodski Z. On program schemata equivalence // Journal of Computer and System Science. — 1972. — v. 6, N 1. — p. 88-101.
16. Котов В.Е., Сабельфельд В.К. Теория схем программ. — М.:Наука, 1991. —
17. с.
18. Eder E. Properties of substitutions and unifications // Journal of Symbolic Computations. — v. 1. — 1985. — p. 31-46.
19. Palamidessi C. Algebraic properties of idempotent substitutions // Lecture Notes in Computer Science — v. 443 — 1990. — p. 386-399.
20. Plotkin G.D. A note on inductive generalization // Machine Intelligence. — 1970. — v. 5, N 1. — p. 153-163.
21. Sorensen M. H., Gluck. R. An algorithm of generalization in positive supercompilation // Proceedings of the 1995 International Symposium on Logic Programming._MIT Press. — 1995. — p. 465-479.
22. Захаров В.А., Костылев Е.В. О сложности задачи антиунификации // Дискретная математика. — 2008. — т. 20, N 1. — с. 131-144.
23. Zakharov V.A. On the refinement of logic programs by means of anti-unification // Proceedings of the 2nd Panhellenic Logic Symposium, Delphi, Greece. — 1999. — p. 219-224.
24. В.А. Захаров, Т.А. Новикова. Применение алгебры подстановок для унификации программ. Труды Института системного программирования РАН,
25. том 21, 2011 г. ISSN 2220-6426 (Online), ISSN 2079-8156 (Print).
Рецензия
Для цитирования:
Захаров В.А., Новикова Т.А. Полиномиальный по времени алгоритм проверки логико-термальной эквивалентности программ. Труды Института системного программирования РАН. 2012;22.
For citation:
Zakharov V.A., Novikova T.A. Polynomial time algorithm for checking strong equivalence of program. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2012;22. (In Russ.)
Послать статью по эл. почте 