• A
  • A
  • A
  • АБB
  • АБB
  • АБB
  • А
  • А
  • А
  • А
  • А
Обычная версия сайта

Статья

Об одной полугрупповой модели программ, определяемой при помощи двухленточных автоматов

В настоящей работе рассматриваются полугруппы программных операторов, подчиняющихся тождествам коммутативности и поглощения. Полугруппы такого вида возникают при решении задач верификации пропозициональных моделей последовательных программ, построенных на основании результатов анализа потоков данных в императивных программах. Установлены необходимые и достаточные условия, при которых отношения равенства операторных цепочек в рассматриваемых полугруппах может быть описано посредством детерминированных двухленточных односторонних автоматов. На основании этих условий получены оценки сложности решения проблемы эквивалентности программ, семантика операторов которых определяется тождествами коммутативности и поглощения.