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

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

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


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

Теорема
• Для всех команд 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.
• Случай [compNS]. Из схемы трансляции имеем:
CS [[S1;S2]] = CS [[S1]] ++ CS [[S2]] .
В правиле [compNS] имеем посылки:
< S1, s> =>s’ и  < S2, s’> =>s”.
Из них по индукции можно заключить:
<CS [[S1]], e, s> #>* < e , e , s’> ,
<CS [[S2]], e, s’> #>* < e , e , s”> .
Выполним код:
 < CS [[S1]] ++ CS [[S2]], e, s>
    #>* < CS [[S2]], e, s’>
    #>* < e , e , s”>
Таким образом случай доказан.



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

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