test/db1/ereftab.lcl

   1 imports employee, eref;
   2
   3 mutable type ereftab;
   4
   5 ereftab ereftab_create(void)
   6 {
   7   /* ensures result' = empty; */
   8 }
   9
  10 void ereftab_insert(ereftab t, employee e, eref er)
  11 {
  12   /* requires getERef(t^, e) = erefNIL; */
  13   modifies t;
  14   /* ensures t' = add(t^, e, er); */
  15 }
  16
  17 bool ereftab_delete(ereftab t, eref er)
  18 {
  19   modifies t;
  20   /* ensures result = in(t^, er) /\ t' = delete(t^, er); */
  21 }
  22
  23 eref ereftab_lookup(employee e, ereftab t)
  24 {
  25   /* ensures result = getERef(t^, e); */
  26 }
  27
  28 void ereftab_initMod(void)
  29 {
  30   ensures true;
  31 }