test/db1/erc.lcl

   1 imports eref;
   2
   3 mutable type erc;
   4 mutable type ercIter;
   5
   6 erc erc_create(void)
   7 {
   8   /* ensures fresh(result) /\ result' = { }; */
   9 }
  10
  11 void erc_clear(erc c)
  12 {
  13   /* requires c^.activeIters = 0; */
  14   modifies c;
  15   /* ensures c' = { }; */
  16 }
  17
  18 void erc_insert(erc c, eref er)
  19 {
  20   /* requires c^.activeIters = 0 /\ er \neq erefNIL; */
  21   modifies c;
  22   /* ensures c' = [insert(er, c^.val), 0]; */
  23 }
  24
  25 bool erc_delete(erc c, eref er)
  26 {
  27   /* requires c^.activeIters = 0; */
  28   modifies c;
  29   /* ensures result = er \in c^.val
  30      /\ c' = [delete(er, c^.val), 0]; */
  31 }
  32
  33 bool erc_member(eref er, erc c)
  34 {
  35   /* ensures result = er \in c^.val; */
  36 }
  37
  38 eref erc_choose(erc c)
  39 {
  40   /* requires size(c^.val) \neq 0; */
  41   /* ensures result \in c^.val; */
  42 }
  43
  44 int erc_size(erc c)
  45 {
  46   /* ensures result = size(c^.val); */
  47 }
  48
  49 ercIter erc_iterStart(erc c)
  50 {
  51   modifies c;
  52   /* ensures fresh(result) /\ result' = [c^.val, c]
  53         /\ c' = startIter(c^);
  54   */
  55 }
  56
  57 eref erc_yield(ercIter it)
  58 {
  59   modifies it; /* , it^.eObj */
  60   /* ensures if it^.toYield \neq { }
  61      then yielded(result, it^, it')
  62        /\ (it^.eObj)' = (it^.eObj)^
  63      else result = erefNIL /\ trashed(it)
  64        /\ (it^.eObj)' = endIter((it^.eObj)^);
  65  */
  66 }
  67
  68 void erc_iterFinal(ercIter it)
  69 {
  70   modifies it; /* , it^.eObj; */
  71   /* ensures trashed(it)
  72      /\ (it^.eObj)' = endIter((it^.eObj)^);
  73   */
  74 }
  75
  76 void erc_join(erc c1, erc c2)
  77 {
  78   /* requires c1^.activeIters = 0; */
  79   modifies c1;
  80   /* ensures c1' = [c1^.val \U c2^.val, 0]; */
  81 }
  82
  83 char *erc_sprint(erc c)
  84 {
  85   /* ensures isSprint(result[]', c^) /\ fresh(result[]); */
  86 }
  87
  88 void erc_final(erc c)
  89 {
  90   modifies c;
  91   /* ensures trashed(c); */
  92 }
  93
  94 void erc_initMod(void)
  95 {
  96   ensures true;
  97 }