test/db1/eref.lcl

   1 imports employee;
   2
   3 immutable type eref;
   4 spec immutable type map;
   5
   6 spec map m;
   7 constant eref erefNIL;
   8
   9 eref eref_alloc(void) map m;
  10 {
  11   modifies m;
  12   /* ensures newInd(result, m^, m'); */
  13 }
  14
  15 void eref_free(eref er) map m;
  16 {
  17   /* requires er \in domain(m^); */
  18   modifies m;
  19   /* ensures m' = delete(m^, er); */
  20 }
  21
  22 void eref_assign(eref er, employee e) map m;
  23 {
  24   /* requires er \in domain(m^); */
  25   modifies m;
  26   /* ensures m' = assign(m^, er, e); */
  27 }
  28
  29 employee eref_get(eref er) map m;
  30 {
  31   /* requires er \in domain(m^); */
  32   /* ensures result = m^[er]; */
  33 }
  34
  35 bool eref_equal(eref er1, eref er2)
  36 {
  37   /* ensures result = (er1 = er2); */
  38 }
  39
  40 void eref_initMod(void) map m;
  41 {
  42   modifies m;
  43   /* ensures m' = new; */
  44 }