Доказать, что естественная семантика языка While – детерминированная (только случаи [ift], [iff], [whilet] и [whilef]). | MetodPro.ru

Реклама на сайте

Доказать, что естественная семантика языка While – детерминированная (только случаи [ift], [iff], [whilet] и [whilef]).


22. Доказать что естественная семантика языка While – детерминированная (только случаи [ass], [skip] и [comp]).
Отношение  <S1,s> -> s’,является функцией.  Для всех S, s, s’, s” из  истинности  <S,s> -> s’и <S,s> -> s”  следует, что s’ = s”. Это значит, что любая команда S языка While и состояние s уникально определяют финальное состояние s’ если выполнение S завершится.
Доказательство.
Предположим что <S,s> -> s’и докажем, что из <S,s> -> s” следует, что s’ = s”. Индуктивное доказательство проведём по дереву вывода для <S,s> -> s’.
Случай [ift]. Состояние s’вычисляется из <if b then S1 else S2,s> -> s’, при условии,  что  B[b]=true и <S1,s> -> s’. Для вычисления <if b then S1 else S2,s> -> s” , можно применить только правило [ift], следовательно, должна выполняться посылка этого правила  <S1,s> -> s”. Применим индуктивную гипотезу: из <S1,s> -> s’ и <S1,s> -> s” получим s’=s” .
Случай [iff] - доказывается аналогично.
Случай [whilet]. Состояние s’вычисляется из <while b do S,s> -> s’, при условии, что  B[b]=true, <S,s> -> s0 и <while b do S, s0> -> s’, для некоторого s0. Для вычисления <while b do S,s> -> s” , можно применить только правило [whilet] (т.к. B[b]=true), следовательно должны выполняться посылки этого правила  <S,s> -> s1 и <while b do S, s1> -> s” для некоторого состояния s1. Применим индуктивные гипотезы:  из <S,s> -> s0 и <S,s> -> s1 получим s0=s1, а из <while b do S, s0> -> s’, и <while b do S, s0> -> s” что s’=s”
Случай [whilef] - доказывается аналогично [skip] .



Методические пособия

  • Системы автоматизированного проектирования
  • Социология молодёжи
  • Общая социология
  • Криптография
  • Проектирование трансляторов
  • Компьютерная графика
  • Моделирование систем
  • Информационная безопасность
  • Теория вычислительных процессов
  • Логические основы искусственного интелекта
  • Проектирование распределённых информационных систем