1 imports employee, eref;
5 only ereftab ereftab_create(void)
7 /* ensures result' = empty; */
10 void ereftab_insert(ereftab t, employee e, eref er)
12 /* requires getERef(t^, e) = erefNIL; */
14 /* ensures t' = add(t^, e, er); */
17 bool ereftab_delete(ereftab t, eref er)
20 /* ensures result = in(t^, er) /\ t' = delete(t^, er); */
23 eref ereftab_lookup(employee e, ereftab t)
25 /* ensures result = getERef(t^, e); */
28 void ereftab_initMod (void) internalState;
30 modifies internalState;
34 iter ereftab_elements(ereftab s, yield eref x);