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.