Preview

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

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

Полиномиальный по времени алгоритм проверки логико-термальной эквивалентности программ

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

Аннотация

Логико-термальная эквивалентность программ - это одно из наиболее слабых отношений эквивалентности программ, аппроксимирующих отношение функциональной эквивалентности и обладающих разрешающим алгоритмом. В данной статье предложена новая модификация алгоритма проверки логико-термальной эквивалентности программ, основанная на операции вычисления точной нижней грани в решетке конечных подстановок. Показано, что трудоемкость предложенного алгоритма оценивается величиной 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.)

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


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


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