Сборники трудов ИСП РАН


Полиномиальный алгоритм проверки эквивалентности в модели программ с перестановочными и подавляемыми операторами.

В.В. Подымов, В.А.Захаров.

Аннотация

В статье исследована задача проверки эквивалентности последовательных программ, некоторые операторы которых обладают свойствами перестановочности и подавления. Два оператора считаются перестановочными, если результат их последовательного выполнения не зависит от порядка, в котором эти операторы выполняются. Считается, что оператор b подавляет оператор a, если последовательное выполнение операторов a и b дает такой же результат, что и выполнение одного лишь оператора b. Разрешимость проблемы эквивалентности в исследуемой модели программ была установлена в 1971 г. А.А. Летичевским. Однако с тех пор вопрос о сложности проверки эквивалентности таких программ оставался открытым. Основной результат статьи – алгоритм, осуществляющий проверку эквивалентности программ с перестановочными и подавляемыми операторами за время, полиномиально зависящее от размеров анализируемых программ.

Ключевые слова

программа, перестановочные операторы, подавляемые операторы, эквивалентность программ, конечный автомат, разрешающий алгоритм, полиномиальная сложность

Издание

Труды Института системного программирования РАН, том 26, вып. 3, 2014, стр. 145-166.

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

DOI: 10.15514/ISPRAS-2014-26(3)-8

Полный текст статьи в формате pdf Вернуться к содержанию тома