Об одном обобщении подстановки применительно к вычислению инвариантов программ.
Об одном обобщении подстановки применительно к вычислению инвариантов программ.
Авторы
Аннотация
Одной из важных задач анализа программ является задача вычисления инвариантов, то есть отношений между данными, которые выполняются для любых вычислений программы. Знание инвариантов необходимо для решения практических задач верификации, оптимизации, синтеза и реорганизации (рефакторинга) программ. Методы вычисления инвариантов равенства существенно зависят от модели исследуемой программы. Ранее нами был предложен метод вычисления инвариантов равенства одномодульных программ, то есть программ, множество операторов которых не содержит вызовов процедур. Этот метод основан на многократном применении операции антиунификации подстановок. Важным свойством, позволяющим применять антиунификацию подстановок для вычисления инвариантов равенства, является выполнимость закона левой дистрибутивности композиции подстановок относительно операции антиунификации. В то же время, закон правой дистрибутивности композиции относительно антиунификации для подстановок в общем случае неверен. Это затрудняет применение антиунификации подста-новок для вычисления инвариантов равенства в программах с рекурсивным вызовом процедур (многомодульных программах). В настоящей заметке предложено новое обобщение подстановок, для которого операция антиунификации удовлетворяет более широкому спектру алгебраических законов (в том числе, закону правой дистрибутивности). Благодаря этому, обобщенные подстановки можно использовать для вычисления инвариантов равенства многомодульных программ.
Ключевые слова
Издание
Труды Третьей Всероссийской конференции «Методы и средства обработки информации», Москва, 2009, Москва, с. 123-130.
Научная группа
Все публикации за 2009 год
Все публикации