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)

Here are the same axioms expressed in ML syntax so you can try executing them with the ML interpreter.