MACHINE Dictionary

/* B specification of a simple Dictionary 
   Michael Butler 13/11/06  */

SETS        Word = {w1,w2,w3,w4,w5}

VARIABLES   known

INVARIANT known : POW(Word)

INITIALISATION  known := {} 

OPERATIONS


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

insert( w ) = 
     PRE w : Word THEN known  :=  known  \/  { w } END ;

delete( w ) = 
     PRE w : Word THEN known  :=  known  -  { w } END
     
END