Go backward to Command Blocks Go up to Top Go forward to Semantics of Command Block

Store Algebra

Store = {<n₁, n₂, ..., n_m> |
   n_i in Int, 1 <= i <= m, m >= 0}

lookup: Location x Store x Int
   lookup(loc_i, <n₁, ..., n_i, ..., n_m>) = n_i
update: Location x Int x Store -> Store
   update(loc_i, n, <n₁, ..., n_i, ..., n_m>)
   = <n₁, ..., n, ..., n_m>
allocate: Store -> Location x Store
   allocate <n₁, n₂, ..., n_m>
   = (loc_m+1, <n₁, n₂, ..., n_m, init>
      where init is some unknown integer
size-of: Store -> Int
   size-of <n₁, n₂, ..., n_m> = m
free: Int -> Store -> Store
free i <n₁, n₂, ..., n_i, ..., n_m> = <n₁, n₂, ..., n_i>
      if 0 <= i <= m