Корректность реализации транслятора языка While. Доказать, что если <S,s> =>s’, то <CS[S], e, s> #>k <e , e , s’>. Случаи if. | MetodPro.ru

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

Корректность реализации транслятора языка While. Доказать, что если =>s’, то #>k . Случаи if.


43) Корректность реализации транслятора языка While. Доказать, что если
<S,s> =>s’, то <CS[[S]], e, s> #>k <e , e , s’>. Случаи if.

Теорема
• Для всех команд S языка While истинно:
SNS [[S]] = SAM [[S]]  .
• Доказательство имеет две части:
1) Если <S,s> =>s’ , то <CS [[S]], e, s> #>k <e , e , s’>
2) Если <CS [[S]], e, s> #>k <e , e, s’> , то <S,s> =>s’ ,
     и e=e.
• Случай [ifttNS].
 Допустим <if b then S1 else S2, s> => s’.
 Поскольку  B [[b]]s = tt, то <S1, s> => s’.
 В результате трансляции получим:
 CS [[if b then S1 else S2]] =
    CB [[b]] ++ BRUNCH(CS [[S1]], CS [[S2]]).
• Выполним код:
 < CB [[b]] ++ BRUNCH(CS [[S1]], CS [[S2]]), e, s>
    #>* < BRUNCH(CS [[S1]], CS [[S2]]), B [[b]]s , s>
    #> <CS [[S1]]),  e, s> (используем инд. гип.)
    #>* < e , e , s’>
Таким образом случай доказан.
• Случай [ifffNS] аналогичен.



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

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