Full Language
E ::= E1:=E2 | E1;E2 | if E1 then E2
else E3 fi
| skip
| while E1 do E2 od | E1+E2
| E1=E2
| not E | @E | N | L
| I=E |E1,E2 | with E1 do
E2 | I | lambdaI:theta. E | E1 E2
theta ::= tauexp | comm | intloc |
pi | theta1 -> | theta2
tau ::= int | bool
pi ::= {j:thetaj}j in J
pi |- E1: intloc | pi |- E2: intexp |
pi |- E1:=E2: comm
|
pi |- E1: comm | pi |- E2: comm |
pi |- E1;E2: comm
|
pi |- E1: boolexp | pi |- E2: comm | pi |- E3: comm |
pi |-
if E1 then E2 else E3 fi:
comm
|
pi |- E1: boolexp | pi |- E2: comm |
pi |-
while E1 do E2 od: comm
|
pi |- E1: intexp | pi |- E2: intexp |
pi |- E1+E2: intexp
|
Author: Wolfgang Schreiner
Last Modification: May 14, 1998