test/db3/empset.lcl

   1 imports employee;
   2 mutable type empset;
   3
   4 only empset empset_create(void)
   5 {
   6   /* ensures fresh(result) /\ result' = { }; */
   7 }
   8
   9 void empset_final (only empset s)
  10 {
  11   modifies s;
  12   /* ensures trashed(s); */
  13 }
  14
  15 void empset_clear(empset s)
  16 {
  17   modifies s;
  18   /* ensures s' = { }; */
  19 }
  20
  21 | bool : void | empset_insert (empset s, employee e) internalState;
  22 {
  23   modifies s, internalState;
  24   /* ensures result = ~(e \in s^) /\ s' = insert(e, s^); */
  25 }
  26
  27 void empset_insertUnique (empset s, employee e) internalState;
  28 {
  29   /* requires ~(e \in s^); */
  30   modifies s, internalState;
  31   /* ensures s' = insert(e, s^); */
  32 }
  33
  34 | bool : void | empset_delete(empset s, employee e)
  35 {
  36   modifies s;
  37   /* ensures result = e \in s^ /\ s' = delete(e, s^); */
  38 }
  39
  40 only empset empset_union(empset s1, empset s2) internalState;
  41 {
  42   modifies internalState;
  43   /* ensures result' = s1^ \U s2^ /\ fresh(result); */
  44 }
  45
  46 only empset empset_disjointUnion (empset s1, empset s2) internalState;
  47 {
  48   modifies internalState;
  49   /* requires s1^ \I s2^ = { }; */
  50   /* ensures result' = s1^ \U s2^ /\ fresh(result); */
  51 }
  52
  53 void empset_intersect (empset s1, empset s2) internalState;
  54 {
  55   modifies s1, internalState;
  56   /* ensures s1' = s1^ \I s2^; */
  57 }
  58
  59 int empset_size(empset s)
  60 {
  61   /* ensures result = size(s^); */
  62 }
  63
  64 bool empset_member(employee e, empset s)
  65 {
  66   /* ensures result = e \in s^; */
  67 }
  68
  69 bool empset_subset(empset s1, empset s2)
  70 {
  71   /* ensures result = s1^ \subseteq s2^; */
  72 }
  73
  74 employee empset_choose(empset s)
  75 {
  76   /* requires s^ \neq { }; */
  77   /* ensures result \in s^; */
  78 }
  79
  80 only char *empset_sprint(empset s)
  81 {
  82   /* ensures isSprint(result[]', s^) /\ fresh(result[]); */
  83 }
  84
  85 void empset_initMod (void) internalState;
  86 {
  87   modifies internalState;
  88   ensures true;
  89 }
  90
  91 iter empset_elements (empset s, yield employee x);