UNC-CH COMP 410
MAP ADT: Axiomatic definition
MAP of ELT, KYT
operations
new : --> MAP
add : MAP x KYT x ELT --> MAP
del : MAP x KYT --> MAP
get : MAP x KYT --> ELT U null
empty : MAP --> boolean
clear : MAP --> MAP
size : MAP --> nat
hasKey : MAP x KYT --> boolean
hasVal : MAP x ELT --> boolean
behavior
get(new, k) = null
get(add(M,k,e), g) = if (k=g) then e
else get(M,g)
empty(new) = true
empty(add(M,k,e)) = false
clear(new) = new
clear(add(M,k,e)) = new
del(new,k) = new
del(add(M,k,e),g) = if (k!=g) then add(del(M,g),k,e)
else if(hasKey(M,k)) then del(M,k)
else M
size(new) = 0
size(add(M,k,e)) = if (hasKey(M,k)) then size(M)
else size(M) + 1
hasKey(new,k) = false
hasKey(add(M,k,e),g) = if (k=g) then true
else hasKey(M,g)
hasVal(new,v) = false
hasVal(add(M,k,e), v) = if (e=v) then true
else hasVal(M,v)