ereftab.lcl

imports employee, eref;
 
mutable type ereftab; 
 
uses ereftab;
 
ereftab ereftab_create(void) {
   ensures result' = empty;
   }
void ereftab_insert(ereftab t, employee e, eref er) {
   requires getERef(t^, e) = erefNIL;
   modifies t;
   ensures t' = add(t^, e, er);
   }
bool ereftab_delete(ereftab t, eref er) {
   modifies t;
   ensures result = in(t^, er) /\ t' = delete(t^, er);
   }
eref ereftab_lookup(employee e, ereftab t) {
   ensures result = getERef(t^, e);
   }
void ereftab_initMod(void) {
    ensures true;
    }