MACHINE Phonebook

/* B specification of a simple Phone book 
   Michael Butler 24/11/06  */

SETS
    Person ; PhoneNum 

VARIABLES dir

INVARIANT
        dir : Person <-> PhoneNum

INITIALISATION  
    dir := {}
    
OPERATIONS

AddEntry(p,n) =
    PRE
        p : Person & 
        n : PhoneNum
    THEN
        dir := dir \/ { p |-> n }
    END;

RemovePerson(p) =
    PRE
        p : Person
    THEN
        dir := {p} <<| dir
    END ;

RemoveNumber(n) =
    PRE
        n : PhoneNum
    THEN
        dir := dir |>> {n}
    END ;

res <-- IsKnown(p) =
    PRE
        p : Person
    THEN
        res := bool( p:dom(dir) )
    END;


nums <-- GetNumbers(p) =
    PRE
        p : Person
    THEN
        nums := dir[ {p} ]
    END;

nums <-- GetMultiNumbers(ps) =
    PRE
        ps <: Person
    THEN
        nums := dir[ ps ]
    END;

peo <-- GetNames(n) =
    PRE
        n : PhoneNum
    THEN
        peo := dir~[ {n} ]
    END;

peo <-- GetMultiNames(ns) =
    PRE
        ns <: PhoneNum
    THEN
        peo := dir~[ ns ]
    END 


END