;--------------------------------------------------------------------
;

TYPE

S = A -> B;
A = ANY;
B = ANY;

ENDTYPE

;--------------------------------------------------------------------
;

FUNC INIT()
STATE S <- [];

FUNC INS(a:A,b:B)
PRE a notin dom(S)
STATE S <- S + [a->b];

FUNC REM(a:A)
STATE S <- S \ {a};

FUNC FIND(a:A):B
PRE a in dom(S)
RETURN S[a];

FUNC EMPTY():Bool
RETURN S == [];