MACHINE CountingDictionary

/* B specification of a counting dictionary 
   Michael Butler 13/11/06  */

SETS        Word

VARIABLES   known, count

INVARIANT 
    known : POW(Word) & 
    count : NATURAL & 
    count = card(known)

INITIALISATION  
    known:={}  ||  count:=0

OPERATIONS


r <-- member( w ) =
     PRE w : Word THEN 
        r := bool(w:known) 
     END ;

insert( w ) = 
     PRE w : Word & w/:known THEN 
        known  :=  known  \/  { w }  || 
        count := count+1
     END ;

delete( w ) = 
     PRE w : Word  & w : known  THEN 
        known  :=  known  -  { w }   || 
        count := count-1
     END
     
END