{\small\sf class} $Directory$
\par
\kTypes
\type{\kw{ }KeyType}{\Token ;}
\type{\kw{ }ValueType}{\Token }
\kInstanceVarDef
\parlinebr
\begin{insvar}
\assdef{my-keys}{\seqof*{KeyType}}[{\seq{}}]
\end{insvar}
\begin{instinvfn}
 \Len my-keys = count\end{instinvfn}
\begin{instinvfn}
\all{i,j \In  \Inds my-keys} \\
{i \Neq j \Implies \fnapply{my-keys}{i} \Neq \fnapply{my-keys}{j}}\end{instinvfn}
\begin{insvar}
\assdef{my-values}{\seqof*{ValueType}}[{\seq{}}]
\end{insvar}
\begin{instinvfn}
 \Len my-values = count\end{instinvfn}
\begin{insvar}
\assdef{count}{\Nat }[{0}]
\end{insvar}
\par
\kOperations
\begin{op}[e]{getCount}%
\signature{() \Oto \Nat }
\parms{}
\annlab[o]{Directory`getCount}
\return{count};
\end{op}
\begin{op}[e]{has}%
\signature{KeyType \Oto \Bool }
\parms{k}
\annlab[o]{Directory`has}
\return{\pex{k \In  \Elems my-keys}};
\end{op}
\begin{op}[e]{value-for}%
\signature{KeyType \Oto ValueType}
\parms{k}
\annlab[o]{Directory`value-for}
\return{\fnapply{my-values}{\iota{i \In  \Inds my-keys}{\fnapply{my-keys}{i} = k}}}
\begin{precond}
\fnapply{has}{k}
\end{precond};
\end{op}
\begin{op}[e]{put}%
\signature{KeyType \X ValueType \Oto ()}
\parms{k,v}
\annlab[o]{Directory`put}
\begin{blockstmt}
\ass{my-keys}{my-keys \Sconc \seq{k}} ; \\
\ass{my-values}{my-values \Sconc \seq{v}} ; \\
\ass{count}{count + 1}
\end{blockstmt}
\begin{precond}
 \Not \fnapply{has}{k}
\end{precond} \\

\post{\fnapply{has}{k} \And  \\
\fnapply{value-for}{k} = v \And  \\
 \Elems \old{my-keys} \Union \set{k} =  \Elems my-keys \And  \\
\all{ki \In  \Inds \old{my-keys}} \\
{\fnapply{\old{my-values}}{ki} = \fnapply{value-for}{\fnapply{\old{my-keys}}{ki}}}};
\end{op}
\begin{op}[e]{remove}%
\signature{KeyType \Oto ()}
\parms{k}
\annlab[o]{Directory`remove}
\begin{blockstmt}
\begin{letstmt}
\patdef{length}{ \Len my-keys}
\end{letstmt} \\
\begin{letstmt}
\patdef{pos}{\iota{i \In  \Inds my-keys}{\fnapply{my-keys}{i} = k}}
\end{letstmt} \\
\begin{blockstmt}
\ass{my-keys}{\subseq{my-keys}{1}{pos \Minus 1} \Sconc \subseq{my-keys}{pos + 1}{length}} ; \\
\ass{my-values}{\subseq{my-values}{1}{pos \Minus 1} \Sconc \subseq{my-values}{pos + 1}{length}} ; \\
\ass{count}{count \Minus 1}
\end{blockstmt}
\end{blockstmt}
\begin{precond}
\fnapply{has}{k}
\end{precond} \\

\post{ \Not \fnapply{has}{k} \And  \\
 \Elems \old{my-keys} =  \Elems my-keys \Union \set{k} \And  \\
\all{ki \In  \Inds my-keys} \\
{\fnapply{my-values}{ki} = \fnapply{\old{my-values}}{\iota{i \In  \Inds \old{my-keys}} \\
{\fnapply{\old{my-keys}}{i} = \fnapply{my-keys}{ki}}}}}
\end{op}
{\small\sf end} {\it Directory}

