Go backward to Abstract Syntax Go up to Top Go forward to Type-Structures |
[[P |- var I: {I:intloc}dec]]e s =
({I=l}, s')
where (l, s') = allocate(s)
and allocate: Store ->
(Location
x Store)
allocate <n1, n2, ..., nm>=
(locm+1, <n1, n2, ..., nm,
init>)
where init is some arbitrary integer
[[P |- define I=U: {I:H}dec]]e s =
({I=f}, s)
where f s' = [[P |- U: H]]e s'
[[D in C: comm]]s = [[P |-C: comm]]e1
s1,
where (e1, s1) = [[{} |- D:
Pdec]]{} s