test/db1/empset.lcl

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