class Directory

types

KeyType = token;

ValueType = token

instance variables

my-keys : KeyType^{∗} := []; inv len my-keys = count inv ∀ i, j ∈ inds my-keys ·

i ≠ j ⇒ my-keys (i) ≠ my-keys (j ) my-values : ValueType^{∗} := []; inv len my-values = count count : ℕ := 0;

operations

getCount : () →^{o} ℕ getCount () \underline{△}

return count; has : KeyType →^{o} 𝔹 has (k) \underline{△}

return (k ∈ elems my-keys); value-for : KeyType →^{o} ValueType value-for (k) \underline{△}

return my-values (ι i ∈ inds my-keys · my-keys (i) = k) pre has (k) ; put : KeyType × ValueType →^{o} () put (k, v) \underline{△}

( my-keys := my-keys ↷ [k]; my-values := my-values ↷ [v]; count := count + 1

) pre ¬ has (k)

post

has (k) ∧ value-for (k) = v ∧

elems \begin{matrix}↼− \\ my-keys \end{matrix} ∪ \{k\} = elems my-keys ∧

∀ ki ∈ inds \begin{matrix}↼− \\ my-keys \end{matrix} · \begin{matrix}↼− \\ my-values \end{matrix} (ki) = value-for (\begin{matrix}↼− \\ my-keys \end{matrix} (ki)); remove : KeyType →^{o} () remove (k) \underline{△}

( let length = len my-keys in let pos = ι i ∈ inds my-keys · my-keys (i) = k in ( my-keys := my-keys (1, …, pos−1)↷my-keys (pos+1, …, length); my-values := my-values (1, …, pos−1)↷my-values (pos+

1, …, length);

count := count − 1 )

) pre has (k)

post

¬ has (k) ∧

elems \begin{matrix}↼− \\ my-keys \end{matrix} = elems my-keys ∪ \{k\} ∧ ∀ ki ∈ inds my-keys ·

my-values (ki) = \begin{matrix}↼− \\ my-values \end{matrix} (ι i ∈ inds \begin{matrix}↼− \\ my-keys \end{matrix} ·

\begin{matrix}↼− \\ my-keys \end{matrix} (i) = my-keys (ki))

end Directory