Go backward to
Store Algebra
Go up to
Top
Go forward to
Scope
Semantics of Command Block
Semantics:
[[
pi
|-
begin
D
in
C
end
:
comm
]]
e
s
=
free
(
size-of
s
)
s
2
where (
e
1
,
s
1
) = [[
pi
|- D:
pi
1
dec
]]
e
s
and
s
2
= [[
pi
-U-
pi
1
|- C:
comm
]](
e
-U-
e
1
)
s
1
Stack-based store management:
Stack pointer recorded at block entry.
D allocates locations for C.
Storage reduced to initial size at block exit.
Author:
Wolfgang Schreiner
Last Modification: May 14, 1998