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$