Go backward to Semantic Algebras Go up to Top Go forward to Command Semantics |
Store = { (n1, n2, ...,
nm)
| ni in Int, 1 <= i <= m, m
>= 0 }
lookup: Location x Store ->
Int
lookup(locj, (n1, n2, ...,
nj, ..., nm)) = nj
(if j>m, then lookup(locj, (n1,
..., nm)) = 0)
update: Location x Int
x Store -> Store
update(locj, j, (n1, n2, ...,
nj, ..., nm)) =
(n1, n2, ..., n, ...,
nm)
(if j>m, then update(locj, n,
(n1, ..., nm)) =
(n1, n2, ..., nm))
if: Bool x
Storebottom x
Storebottom ->
Storebottom
if(true, s1, s2) = s1
if(false, s1, s2) = s2
(Storebottom = Store
union {bottom},
bottom = "bottom" = non-termination)