Go backward to
Semantics of Lazy Evaluation
Go up to
Top
Go forward to
Other Standard Abstractions
Semantics of Eager Evaluation
Store is given when function is defined.
[[
p
|-
define
I=U: {I:
H
}
dec
]]
e
s
= {I=[[
p
|-U:
H
]]
e
s
.
[[
p
|-
invoke
I:
H
]]
e
s
=
v
,
where (I=
v
) in
e
.
Example:
[[
p
|-
const
I=E: {I:
T
exp
}]]
e
s
= {I=[[
p
|- E:
T
exp
]]
e
s
}.
[[
p
|- I:
T
exp
]]
e
s
=
v
,
where (I=
v
) in
e
.
Improper meaning for body:
[[
p
|-
loop
:
intexp
]]
e
s
=
bottom
.
[[
p
|-
fun
A
=
loop
in skip
:
comm
]]
e
s
= [[ {
A
:
intexp
} |-
skip
:
comm
]]
e
0
s
,
where
e
0
= {
A
=[[{}|-
loop
:
intexp
]]{}
s
}
= {
A
=
bottom
= [[{
A
:
intexp
} |-
skip
:
comm
]]
bottom
s
=
bottom
.
Author:
Wolfgang Schreiner
Last Modification: April 2, 1998
