MACHINE Birthdaybook

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

SETS
    Person ; Date 

VARIABLES known, bb

INVARIANT
        known : POW(Person) &
        bb : known --> Date

INITIALISATION  
    known := {}  ||  bb := {}
    
OPERATIONS

AddEntry(p,d) =
    PRE
        p : Person & 
        p /: known &
        d : Date
    THEN
        known := known \/ {p} ||
        bb := bb \/ { p |-> d }
    END;

UpdateEntry(p,d) =
    PRE
        p : known &
        d : Date
    THEN
        bb(p) := d
    END;

RemovePerson(p) =
    PRE
        p : Person
    THEN
        known := known \ {p}  ||
        bb := {p} <<| bb
    END ;

res <-- LookupPerson(p) =
    PRE
        p : known
    THEN
        res := bb(p)
    END;


res <-- LookupDate(d) =
    PRE
        d : Date
    THEN
        res := bb~[ {d} ]
    END


END