previous up next
Go backward to Sum Domains
Go up to Top
Go forward to Function Domains
RISC-Linz logo

Function Domains

Dynamic arrays

Domain Array = Nat -> A
where A is a domain with an error element
Operations
newarray: 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)


Author: Wolfgang Schreiner
Last Modification: October 14, 1997

previous up next