Об одном обобщении подстановки применительно к задаче статического анализа программ.
Об одном обобщении подстановки применительно к задаче статического анализа программ.
Авторы
Аннотация
Одной из задач статического анализа программ является поиск инвариантных соотношений, которые затем могут быть использованы для верификации, оптимизации, специализации программ и пр. Среди различных инвариантных соотношений особое место занимают отношения равенства термов (выражений). На первом этапе проекта для решения этой задачи был предложен метод вычисления инвариантов равенства, в основу которого был положен алгоритм антиунификации термов, связанный с вычислением точной нижней грани подстановок. Недостатком этого метода является то, что операция взятия точной нижней грани не обладает свойством дистрибутивности относительно операции композиции подстановок. Поэтому данный метод не обладает модульным свойством, и в случае анализа программ с рекурсивными процедурами его нельзя применять независимо ко всем модулям программы. Для преодоления этой трудности нами было предложено новое понятие метаподстановки, обобщающее хорошо известное понятие подстановки. Метаподстановка представляет собой множество подстановочных шаблонов, из которых могут конструироваться подстановки. Были исследованы алгебраические и теоретико- решетчатые свойства метаподстановок и установлено, что для метаподстановок соблюдается закон дистрибутивности операции взятия точной нижней грани относительно операции композиции.
Издание
Вестник Московского университета. Серия 15. Вычислительная математика и кибернетика, 2005, том 4, с. 39-45.
Научная группа
Все публикации за 2005 год
Все публикации