Естественная семантика языка While. | MetodPro.ru

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

Естественная семантика языка While.


19. Естественная семантика языка While. Семантическая эквивалентность операторов языка While. Доказать эквивалентность операторов while b do S и if b then (S; while b do S) else skip.
Отношение «вычисляет» имеет вид: <S,s> -> s’, где S – команда, s - состояние переменных.
Правила
[ass] <x:=e,s> -> s[x/A[e]s], где A[e]s обозначает s |- e ->A v
[skip] < skip,s> -> s.
[comp] [дробь][числитель]<S1,s> -> s’, <S2,s’> -> s” [/ числитель][знаменатель]<S1;S2,s> -> s”[/ знаменатель][/дробь]
[ift] [дробь][числитель]<S1,s> -> s’ [/ числитель][знаменатель]<if b then S1 else S2,s> -> s’ [/ знаменатель][/дробь] при [B[b]s=T], где B[b]s=bv обозначает s |- b ->B bv
[iff] [дробь][числитель]<S2,s> -> s’ [/ числитель][знаменатель]<if b then S1 else S2,s> -> s’ [/ знаменатель][/дробь] при [B[b]s=F], где B[b]s=bv обозначает s |- b ->B bv
[whilet] [дробь][числитель]<S,s> -> s’ <while b do S, s’> -> s” [/ числитель][знаменатель][/ знаменатель] <while b do S,s> -> s” [/дробь] при [B[b]s=T], где B[b]s=bv обозначает s |- b ->B bv
[whilef] [дробь][числитель][/ числитель][знаменатель]<while b do S,s> -> s [/ знаменатель][/дробь] при [B[b]s=F], где B[b]s=bv обозначает s |- b ->B bv
Семантическая эквивалентность операторов
Операторы S1 и S2 семантически эквивалентны, если для любых двух состояний s и s’ справедливо: <S1,s>-> s’ ? <S2,s> -> s’. Докажем, что операторы while b do S и if b then (S; while b do S) else skip семантически эквивалентны.
Доказательство
Часть 1
Докажем, что если <while b do S, s> -> s” (1) то и < if b then (S; while b do S) else skip, s> -> s” (2). Из истинности посылки (1) следует, что для неё существует дерево вывода T. Корень этого дерева может иметь одну из двух форм, в зависимости от того, использовалось ли правило [whilet] или [whilef] . В первом случае дерево T , будет иметь форму: [дробь][числитель]T1          T2[/ числитель][знаменатель]<while b do S,s> -> s’’ [/ знаменатель][/дробь], где T1 -  дерево вывода с корнем <S,s> -> s’, а T2 - имеет корень <while b do S, s’> -> s” более того B[b]s=T. Использовав T1 и T2 как посылки правила [comp] получим дерево: [дробь][числитель]T1          T2[/ числитель][знаменатель]<S; while b do S,s> -> s’’ [/ знаменатель][/дробь]. Учитывая, что B[b]s=T можно применив правило [ift] получим дерево: [дробь][числитель] [дробь][числитель]T1          T2[/ числитель][знаменатель]<S; while b do S,s> -> s’’ [/ знаменатель][/дробь] [/ числитель][знаменатель] if b then (S; while b do S) else skip,s> -> s’’ [/ знаменатель][/дробь] В нём получился вывод заключения (2).
Во втором случае, когда использовалось правило [whilef] и выполнялось условие B[b]s=F, тогда s = s”. Дерево T будет иметь форму: <while b do S, s> -> s. Используя аксиому [skip] получим <skip,s> ==> s, а применив правило [iff] получим дерево вывода для (2):
[дробь][числитель] <skip, s> -> s [/ числитель][знаменатель] if b then (S; while b do S) else skip,s> -> s [/ знаменатель][/дробь] В нём получился вывод заключения (2), если учесть, что s = s”. Это завершает доказательство первой части.
Часть 2
Докажем импликацию в обратном порядке: если < if b then (S; while b do S)     else skip, s> -> s” (2) то и <while b do S, s> -> s”(1). Для этого, имея дерево вывода T для (2), нужно построить дерево вывода для (1). Для (2) дерево вывода могло быть построено только правилами [ift] или [iff].
В первом случае, когда B[b]s=T, вершина (2) получена из вершины T1 = < S; while b do S, s> -> s”, которая , в свою очередь как композиция операторов могла быть получена только по правилу [comp] . Значит к T1 ведут две ветви:    T2 = < S, s> -> s’, T3 = < while b do S, s’> -> s”. Теперь, если T2 и T3 в качестве посылок для правила [whilet] получим дерево вывода для (1). Во втором случае, когда выполнялось условие  B[b]s=F, дерево T будет строиться по правилу [iff] и, тогда получим ветвь для <skip, s> -> s”. На основании аксиомы [skip] получим, что  s = s” . Теперь, применив аксиому [whilef] получим дерево вывода для (1).



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

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