UNC-CH COMP 410

MAP ADT: Axiomatic definition

MAP of ELT, KYT

operations

   new    :                  --> MAP
   put    : MAP x KYT x ELT  --> MAP

   get    : MAP x KYT        --> ELT U null
   isEmpty: MAP              --> boolean
   clear  : MAP              --> MAP
   remove : MAP x KYT        --> MAP
   size   : MAP              --> nat
   hasKey : MAP x KYT        --> boolean
   hasVal : MAP x ELT        --> boolean
   

behavior
   get(new, k) = null
   get(put(M,k,e), g) = if (k=g) then e
                                 else get(M,g)

   isEmpty(new) = true
   isEmpty(put(M,k,e)) = false

   clear(new) = new
   clear(put(M,k,e)) = new

   remove(new,k) = new
   remove(put(M,k,e),g) = if (k!=g) then put(remove(M,g),k)
                                    else if(hasKey(M,k)) then remove(M,k)
                                                         else M

   size(new) = 0
   size(put(M,k,e)) = if (hasKey(M,k)) then size(M)
                                       else size(M) + 1

   hasKey(new,k) = false
   hasKey(put(M,k,e),g) = if (k=g) then true
                                   else hasKey(M,g)

   hasVal(new,v) = false
   hasVal(put(M,k,e), v) = if (e=v) then true
                                    else hasVal(M,v)