|
Slide 9.6: An assignment example Slide 9.8: A control example Home |
|
P ::= L L ::= S ';' L1 | S S ::= I ':=' E | 'if' E 'then' L1 'else' L2 'fi | 'while' E 'do' L 'od'Reduction rules for if-statements are the following:
<E|Env> ⇒ <E1|Env>
<'if' E 'then' L1 'else' L2 'fi' | Env> ⇒ <'if' E1 'then' L1 'else' L2 'fi' | Env>
V > 0
<'if' V 'then' L1 'else' L2 'fi' | Env> ⇒ <L1 | Env> V ≤ 0
<'if' V 'then' L1 'else' L2 'fi' | Env> ⇒ <L2 | Env> <E|Env> ⇒ <V|Env>, V≤0
<'while' E 'do' L 'od' | Env> ⇒ Env <E|Env> ⇒ <V|Env>, V>0
<'while' E 'do' L 'od' | Env> ⇒
<L ; 'while' E 'do' L 'od' | Env>Env, the expression E evaluates to a positive value, then execution of the while-loop under Env reduces to an execution of L, followed by the execution of the same while-loop all over again.