Об одном обобщении подстановок применительно к задаче синтеза инвариантов программ.
Об одном обобщении подстановок применительно к задаче синтеза инвариантов программ.
Авторы
Аннотация
Одной из задач статического анализа программ является поиск инвариантных соотношений, которые затем могут быть использованы для верификации, оптимизации, специализации программ и пр. Среди различных инвариантных соотношений особое место занимают отношения равенства термов (выражений). Для решения этой задачи авторами настоящей заметки ранее был предложен метод вычисления инвариантов равенства, в основу которого был положен алгоритм антиунификации термов, связанный с вычислением точной нижней грани подстановок. Недостатком этого метода является то, что операция взятия точной нижней грани не обладает свойством дистрибутивности относительно операции композиции подстановок, и поэтому данный метод не обладает модульным свойством, позволяющим применять его независимо для нескольких взаимосвязанных модулей программы. Для преодоления этой трудности нами было предложено обобщение понятия подстановки. Исследованы алгебраические и теоретико-решетчатые свойства обобщенных подстановок и установлено, что для обобщенных подстановок соблюдается закон дистрибутивности операции взятия точной нижней грани относительно операции композиции.
Издание
Материалы VIII Международного семинара «Дискретная математика и ее приложения» (Москва, 2-6 февраля 2004 г.), 2004, Изд-во механико-математического ф-та МГУ Москва, с. 134-137.
Научная группа
Все публикации за 2004 год
Все публикации