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

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

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


21. Доказать что естественная семантика языка 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’.
Случай [ass]. S = x:=e, s’= s[x/A[e]s], вычисляется также:  < x:=e,s> -> s”, s’= s[x/A[e]s], следовательно s’ = s”.
Случай [skip] доказывается аналогично.
Случай [comp]. Состояние s’вычисляется из <S1;S2,s> -> s’, используя <S1,s> -> s0, <S2,s0> -> s’, для некоторого s0. Для вычисления <S1;S2,s> -> s” , можно применить только правило [comp]. Следовательно должно существовать состояние s1 такое, что <S1,s> -> s1, <S2,s1> -> s”.
Применим индуктивные гипотезы: из <S1,s> -> s0 и <S1,s> -> s1 получим s0=s1, а из <S2,s0> -> s’ и <S2,s0> -> s” что s’=s”



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

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