test/db3/eref.lcl

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