Go backward to Semantic Algebras Go up to Top Go forward to Command Semantics

Semantic Algebras

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