Проверка эквивалентности программ с помощью двухленточных автоматов

• Published in: Кибернетика и системный анализ
• Date: 2010
• Main Author: Захаров, В.А.
• Format: Article
• Language: Russian
• Published: Інститут кібернетики ім. В.М. Глушкова НАН України 2010
• Subjects: Кибернетика
• Online Access: https://nasplib.isofts.kiev.ua/handle/123456789/45242
• Journal Title: Digital Library of Periodicals of National Academy of Sciences of Ukraine
• Cite this: Проверка эквивалентности программ с помощью двухленточных автоматов / В.А. Захаров // Кибернетика и системный анализ. — 2010. — № 4. — С. 39-48. — Бібліогр.: 44 назв. — рос.

Семантика послідовних програм визначається на основі моделей динамічної логіки. Якщо динамічна шкала ациклічна, її можна описати двострічковим детермінованим автоматом. У такому разі перевірки еквівалентності програм, семантика операторів яких визначається ациклічними динамічними шкалами, зводиться до задачі перевірки порожнистості двострічкових автоматів (комбінованих машин). This paper shows how two-tape automata can be employed to design efficient equivalence checking procedures for sequential programs. The semantics of sequential programs is defined in terms of dynamic logic structures. If the dynamic frame is acyclic (i.e., all program statements are irreversible), it can be specified by means of a two-tape deterministic automaton. Then the equivalence checking problem for sequential programs operating on the dynamic frame can be reduced to the emptiness problem for two-tape automata (compound machine).