Go backward to
Escaping Locations
Go up to
Top
Go forward to
Declaration Blocks
Extent in Other Block Forms
Declaration block (module)
module
M
=
begin var
A
:
newint in
{
proc
INIT
=
A
:=0,
proc
SUCC
=
A
:=@
A
+1
fun
VAL
= @
A
}
end
Location for
A
is allocated when
M
is evaluated.
A
's location must escape declaration block (body of
M
)!
[[
pi
|-
begin
D
1
in
D
2
end
:
pi
2
dec
]]
e
s
=
[[
pi
-U-
pi
1
|- D
2
:
pi
2
dec
]](
e
-U-
e
1
)
s
1
where (
e
1
,
s
1
) = [[
pi
|- D
1
:
pi
1
dec
]]
e
s
Locations allocated within D
1
and D
2
are retained.
Author:
Wolfgang Schreiner
Last Modification: May 14, 1998
