Especificação CAMILA de um Dicionário

interface DIC = 
    sorts Dic, Pal, Sig, Bool; 
    state Dic; 
   events INIT:->, 
          INSPAL:PalxSig->, 
          REMPAL:Pal->, 
          CONSPAL:Pal->Sig,
          EMPTYDIC:->Bool,
          EXISTPAL:Pal->Bool;
end; 

module Dicionario: DIC
 sorts Dic = Pal -> Sig;
       Pal = STR;
       Sig = STR;
       Bool = SYM;
events INIT = 
         sigma' = [];
       INSPAL(pal, sig) = 
         { ~EXISTPAL(pal) => sigma' = sigma + [pal -> sig];
       REMPAL(pal) =
         { EXISTPAL(pal) => sigma' = sigma\{pal};
       CONSPAL(pal, sig') =
         { EXISTPAL(pal) => sig' = sigma[pal];
       EMPTYDIC(b') =
         b' = sigma == [];
       EXISTPAL(pal, b') =
         b' = pal in dom(sigma);
end;