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

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

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


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

Теорема
• Для всех команд 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.
Докажем первую часть
• Докажем индукцией по дереву вывода <S,s> =>s’.
• Случай [assNS]. Имеем <x:=a, s> =>s’ ,
а s’= s[x/A[a]s] .
Из схемы трансляции имеем:
CS [[x:=a]] = CA [[a]] ++ STORE-x.
Из доказанной леммы об арифм. выражениях получим:
<CA [[a]], e, s> #>*< e , A [a]s, s> .
Выполним код:
 <CA [[a]]:STORE-x, e, s>
    #>*< STORE-x , (A [a]s), s>
    #> < e, e,  s[x/A[a]s]>
Поскольку s’= s[x/A[a]s], случай доказан.




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

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