test/db2/erc.lcl

   1 imports eref;
   2
   3 mutable type erc;
   4
   5 erc erc_create(void)
   6 {
   7   /* ensures fresh(result) /\ result' = { }; */
   8 }
   9
  10 void erc_clear(erc c)
  11 {
  12   /* requires c^.activeIters = 0; */
  13   modifies c;
  14   /* ensures c' = { }; */
  15 }
  16
  17 void erc_insert(erc c, eref er)
  18 {
  19   /* requires c^.activeIters = 0 /\ er \neq erefNIL; */
  20   modifies c;
  21   /* ensures c' = [insert(er, c^.val), 0]; */
  22 }
  23
  24 | bool : void | erc_delete(erc c, eref er)
  25 {
  26   /* requires c^.activeIters = 0; */
  27   modifies c;
  28   /* ensures result = er \in c^.val
  29      /\ c' = [delete(er, c^.val), 0]; */
  30 }
  31
  32 bool erc_member(eref er, erc c)
  33 {
  34   /* ensures result = er \in c^.val; */
  35 }
  36
  37 eref erc_choose(erc c)
  38 {
  39   /* requires size(c^.val) \neq 0; */
  40   /* ensures result \in c^.val; */
  41 }
  42
  43 int erc_size(erc c)
  44 {
  45   /* ensures result = size(c^.val); */
  46 }
  47
  48 void erc_join(erc c1, erc c2)
  49 {
  50   /* requires c1^.activeIters = 0; */
  51   modifies c1;
  52   /* ensures c1' = [c1^.val \U c2^.val, 0]; */
  53 }
  54
  55 char *erc_sprint(erc c)
  56 {
  57   /* ensures isSprint(result[]', c^) /\ fresh(result[]); */
  58 }
  59
  60 void erc_final(erc c)
  61 {
  62   modifies c;
  63   /* ensures trashed(c); */
  64 }
  65
  66 void erc_initMod(void)
  67 {
  68   modifies internalState;
  69   ensures true;
  70 }
  71
  72 iter erc_elements (erc c, yield eref el);