Корректность реализации транслятора языка While. Доказать, что если =>s’, то #>k . Случаи while.
44) Корректность реализации транслятора языка While. Доказать, что если
<S,s> =>s’, то <CS[[S]], e, s> #>k <e , e , s’>. Случаи while.
Теорема
• Для всех команд 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.
• Случай [whilettNS].
Допустим <while b do S, s> => s”.
Поскольку B [[b]]s = tt, то <S, s> => s’
и <while b do S, s’> => s”.
В результате трансляции получим:
CS [[while b do S]] =LOOP (CB [[b]], CS [[S]]).
• Выполним код:
< LOOP (CB [[b]], CS [[S]]), e, s> #>
<CB [[b]]++BRUNCH(CS [[S]]++
LOOP(CB [[b]], CS [[S]]), NOOP), e, s>
#>* <BRUNCH(CS [[S]] ++
LOOP (CB [[b]], CS [[S]]), NOOP), B [[b]]s, s>
#> <CS [[S]]++LOOP(CB [[b]], CS [[S]]), e, s>
• В правиле [whilettNS] имеем посылки:
< S, s> =>s’ и <while b do S, s’> => s”.
Из них по индукции можно заключить:
<CS [[S]], e, s> #>* < e , e , s’> ,
<LOOP(CB [[b]], CS [[S]]), ], e, s’> #>* < e , e , s”> .
Выполним код:
< CS [[S]]++ LOOP(CB [[b]], CS [[S]]), e, s>
#>* <LOOP(CB [[b]], CS [[S]]), e, s’>
#>* < e , e , s”>
• Таким образом случай доказан.
• Случай [whileffNS].
Допустим <while b do S, s> => s’.
Поскольку B [[b]]s = ff, то s = s’.
В результате трансляции получим:
CS [[while b do S]] = LOOP (CB [[b]], CS [[S]]).
• Выполним код:
< LOOP (CB [[b]], CS [[S]]), e, s> #>
<CB [[b]]++BRUNCH(CS [[S]]++LOOP(CB [[b]], CS [[S]]), NOOP), e, s>
#>* <BRUNCH(CS [[S]] ++ LOOP (CB [[b]], CS [[S]]), NOOP), B [[b]]s, s>
#> < NOOP, e, s>
#> < e, e, s>
Таким образом случай доказан.