Корректность реализации транслятора языка 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>

Таким образом случай доказан.