Go backward to Sum Domains Go up to Top Go forward to Function Domains |
Dynamic arrays
Domain Array = Nat -> Awhere A is a domain with an error elementOperationsnewarray: Array
newarray = lambda n.error
access: Nat x Array -> A
access(n, r) = r(n)
update: Nat x A x Array -> Array
access(n, v, r) = [n |-> v]r
Bounds are not restricted!
access(m, update(n, v, r)) where m != n
= (update(n, v, r))(m) definition of access
= ([n |-> v]r)(m) definition of update
= (lambda m.(equals m n) -> v [] r(m))(m)
update
= (equals m n) -> v [] r(m) function
application
= false -> v [] r(m)
= r(m)