Consider the ADT \(\texttt{IP}\) (inverted phonebook) which is a set of entries, each consisting in the phone number and the name of a person, that is used to find the person name from his phone number (like True caller):

Type: \(\texttt{IP}\)
Parameter: \(\texttt{Type_number, Type_name}\)
Use: \(\texttt{Boolean}\)

Functions:
\(\begin{array}{p{1cm} l l l l} & \textbf{Create }: & & \rightarrow \texttt{IP}\\ & \textbf{Add}: & \texttt{IP} \times \texttt{Type_number} \times \texttt{Type_name} & \rightarrow \texttt{IP} \\ & \textbf{Is_empty}: & \texttt{IP} & \rightarrow \texttt{Boolean} \\ & \textbf{Delete}: & \texttt{IP} \times \texttt{Type_number} & \rightarrow \texttt{IP} \\ & \textbf{Belong}: & \texttt{IP} \times \texttt{Type_number} & \rightarrow \texttt{Boolean} \\ & \textbf{Find}: & \texttt{IP} \times \texttt{Type_number} & \rightarrow \texttt{Type_name} \\ & \textbf{Modify }: & \texttt{IP} \times \texttt{Type_number} \times \texttt{Type_name} & \rightarrow \texttt{IP } \\ \end{array}\)

Constructors: ...
Preconditions:  

Let $$I$$ an $$IP$$, $$N$$ a \(\texttt{Type_number}\), and $$P$$ a \(\texttt{Type_name}\):

  • \(\texttt{Find(I,N)}\), \(\texttt{Delete(I,N)}\) and \(\texttt{Modify(I,N,P)}\) defined iff \(\texttt{Belong(I,N)}\)
  • \(\texttt{Add(I,N,P)}\) defined iff \(\texttt{not}\) \(\texttt{Belong(I,N)}\)


Axioms: ...

Choose constructors functions and complete axioms.

Difficulty level
This exercise is mostly suitable for students 

Constructors: Create, add

Let R be an IP, N a Type_number, P and Q 2 Type_name
Axioms:
    * Is_empty(Create())=True
    * Is_empty(Add(R,N,P))=False
    * Delete(Add(R,N,P),N)=R
    * Belong(Create(),N)=False
    * Belong(Add(R,N,P),N)=True
    * Find(Add(R,N,P),N)=P
    * Modify(Add(R,N,P),N,Q)=Add(R,N,Q)
Back to the list of exercises
Looking for a more challenging exercise, try this one !!
UVA 1112 - Mice and Maze