Go backward to
Summary (Semantics I)
Go up to
Top
Go forward to
Summary (Semantics III)
Summary (Semantics II)
Declaration
[[
P
|-
define
I=U: {I:
H
}
dec
]]
e
s
= ({I=
f
},
s
)
where
f
s'
= [[
P
|- U:
H
]]
e
s'
and U in{E, T, C}
[[
P
|- D
1
;D
2
: (
P
1
U
P
2
)
dec
]]
e
s
=
(
e
1
union
e
2
,
s
2
)
where (
e
1
,
s
1
) = [[
P
|- D
1
:
P
1
dec
]]
e
s
and (
e
2
,
s
2
) = [[
P
U
P
1
|- D
2
:
P
2
dec
]] (
e
union
e
1
)
s
1
[[
P
|-
fun
I=E: {I:
T
exp
}]]
e
s
= {I=
f
}
where
f(s')
= [[
P
|- E:
T
exp
]]
e
s'
[[
P
|-
const
I=N: {I:
int
}]]
e
s
=
{I=[[
P
|- N:
int
]]
e
s
}.
[[
P
|-
proc
I=C: {I:
comm
}
dec
]]
e
s
= {I=
r
},
where
r(s')
= [[
P
|- C:
comm
]]
e
s'
.
[[
P
|-
var
I:T: {I:
D
}
dec
]]
e
s
= ({I=
v
},
s'
)
where (
v
,
s'
) = [[
P
|- T:
D
class
]]
e
s
.
[[
P
|-
class
I=T: {I:
D
class
}
dec
]]
e
s
= {I=
r
},
where
r(s')
= [[
P
|- T:
D
class
]]
e
s'
.
Author:
Wolfgang Schreiner
Last Modification: April 23, 1998
