previous up next
Go backward to Abstract Syntax
Go up to Top
Go forward to Type-Structures
RISC-Linz logo

Semantics of Variables

[[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

Author: Wolfgang Schreiner
Last Modification: April 23, 1998

previous up next