Expression Abstractions

Expression abstractions = functions.

P in Program	L in Location
D in Declaration	N in Numeral
C in Command	I in Identifier
E in Expression

P ::= D in C
D ::= fun I=E | D_1,D_2 | D_1;D_2
C ::= L:=E | C_1;C_2 | if E then C_1 else C_2 fi
        | while E do C od | skip
E ::= N | @L | E_1+E_2 | E_1=E_2 | not E | I
L ::= loc_i, i>0
N ::= n, n in Int

• New domains Identifier and Declaration.
• Definition: fun I=E.
• Invocation: I.