Semantic Algebras

Store = { (n_1, n_2, ..., n_m)
    | n_i in Int, 1 <=i <=m, m >=0 }
lookup: Location x Store -> Int
    lookup(loc_j, (n_1, n_2, ..., n_j, ..., n_m)) = n_j
    (if j>m, then lookup(loc_j, (n_1, ..., n_m)) = 0)
update: Location x Int x Store -> Store
    update(loc_j, j, (n_1, n_2, ..., n_j, ..., n_m)) =
        (n_1, n_2, ..., n, ..., n_m)
    (if j>m, then update(loc_j, n, (n_1, ..., n_m)) =
        (n_1, n_2, ..., n_m))
if: Bool x Store_bottom x Store_bottom -> Store_bottom
    if(true, s_1, s_2) = s_1
    if(false, s_1, s_2) = s_2
    (Store_bottom = Store union {bottom},
    bottom = "bottom" = non-termination)