Эквивалентность естественной и структурно-операционной семантик языка While. Доказать, что для каждой команды S и любых состояний s и s’ справедливо, что из <S,s > => s’ следует <S,s > ->* s’ (случаи while). | MetodPro.ru

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

Эквивалентность естественной и структурно-операционной семантик языка While. Доказать, что для каждой команды S и любых состояний s и s’ справедливо, что из => s’ следует ->* s’ (случаи while).


31. Эквивалентность естественной и структурно-операционной семантик языка While. Доказать, что для каждой команды S и любых состояний s и s’ справедливо, что из <S,s > => s’ следует <S,s > ->* s’ (случаи while).
Теорема: для каждой команды языка While выполняется равенство Sns[S] = Ssos[S].
Доказательство имеет две части:
1) для каждой команды S и любых состояний s и s’ справедливо, что из <S,s > => s’ следует <S,s > ->* s’;
2) для каждой команды S, любых состояний s и s’ и натурального числа k справедливо, что из <S,s >->k s’ следует <S,s > => s’.
Первая часть доказывается индукцией по структуре дерева вывода <S,s > => s’.
Вторая часть доказывается индукцией по длине последовательности вывода для <S,s >->k s’ .
Случай [whiletns]. Допустим, что <while b do S,s> => s” и B[b]s = true.
Поскольку <S,s> => s’ и <while b do S,s’> => s” то, применив индуктивные гипотезы, получим <S,s> ->* s’ и <while b do S,s’> ->* s”. Так как вычисление первой команды композиции не зависит от второй команды, получим <S; while b do S, s> ->* s”. (1)
Теперь можно построить последовательность вывода:
 <while b do S, s> -> (по правилу [whiletsos])  <if b then (S; while b do S) else skip,s> -> (по правилу [iftsos] )  <S; while b do S, s> ->* (по (1)) s”.
Случай  доказан.
О теореме в целом
Для каждой команды S языка While и состояния s мы доказали, что если Sns[S] s = s’, то Ssos[S]s = s’; и наоборот, если Ssos[S]s = s’, то Sns[S] s = s’.  Этого достаточно для того, чтобы утверждать о равенстве функций, то есть что Sns[S] = Ssos[S].



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

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