Go backward to
Lazy Evaluation Semantics
Go up to
Top
Go forward to
Eager Evaluation Semantics
Variable Declarations
New block construct for variables:
Allocate location, bind it to identifier V and let V be visible to command E.
pi
-U- { V:
intloc
} |- E:
comm
pi
|-
new
V
in
E:
comm
[[
pi
|-
new
V
in
E
:
comm
]]
e
s
=
free
(
size-of
s
)
s
_{2}
where (
l
,
s
_{1}
) =
allocate
s
and
s
_{2}
= [[
pi
-U- { V:
intloc
} |- E:
comm
]]
(
e
-U- { V=
l
})
s
_{1}
Lazy evaluation semantics is preserved.
Author:
Wolfgang Schreiner
Last Modification: May 14, 1998