Semantics of Variables

[[$P$ |- var I: {I:intloc}dec]]$e$ $s$ = ({I=$l$}, $s\text{'}$)
    where ($l$, $s\text{'}$) = allocate($s$)
    and allocate: Store $->$ (Location x Store)
        allocate <$n$₁, $n$₂, ..., $n$_m>=
            (loc$$_m+1, <$n$₁, $n$₂, ..., $n$_m, init>)
        where init is some arbitrary integer

• Abstraction (I=l)
• Command ($s$ $->$ $s\text{'}$)
• Declarations can alter store!

[[$P$ |- define I=U: {I:$H$}dec]]$e$ $s$ = ({I=$f$}, $s$)
    where $f$ $s\text{'}$ = [[$P$ |- U: $H$]]$e$ $s\text{'}$
[[D in C: comm]]$s$ = [[$P$ |-C: comm]]$e$₁ $s$₁,
    where ($e$₁, $s$₁) = [[{} |- D: $P$dec]]{} $s$