Environments and Assignments

We want to extend the operational semantics of expressions to include environments and assignments, according to the following abstract syntax: 
   P ::= L
   L ::= S ';' L1 | S
   S ::= I ':=' E
   E ::= E1 '+' E2 | E1 '–' E2 | E1 '*' E2 | '(' E1 ')' | N
   N ::= N1 D | D
   D ::= '0' | '1' | … | '9'
   I ::= I1 A | A
   A ::= 'a' | 'b' | … | 'z'
To do this we must include the effect of assignments on the storage of the abstract machine. The storage is an environment that is a function from identifiers to integer values (including the undefined value): 
Env: Identifier → Integer ∪ {undef}
To add environments to the reduction rules, we need a notation to show the dependence of the value of an expression on an environment. We use the notation <E|Env> to indicate that expression E is evaluated in the presence of environment Env. Now our reduction rules change to include environments. For example, the Rule 7 in the previous slide is 
  1.          E ⇒ E1         
     E '+' E2 ⇒ E1 '+' E2
the Rule with environments becomes 
  1.            <E|Env> ⇒ <E1|Env>           
     <E '+' E2 | Env> ⇒ <E1 '+' E2 | Env>
This states that if E reduces to E1 in the presence of environment Env, then E '+' E2 reduces to E1 '+' E2 in the same environment. Other rules are modified similarly.