test/db2/empset.h

   1 # ifndef EMPSET_H
   2 # define EMPSET_H
   3
   4 # include "eref.h"
   5 # include "erc.h"
   6 # include "ereftab.h"
   7
   8 typedef erc empset;
   9
  10 ereftab known;
  11
  12 /*
  13   Abstraction function, toEmpSet:
  14     e \in toEmpSet(s) ==
  15       exists er (count(er, s.val) = 1
  16         /\ getERef(known, e) = er)
  17
  18   Rep invariant:
  19     forall s: empset
  20       (forall er: eref (count(er, s.val) <= 1)
  21       /\ s.activeIters = 0
  22       /\ forall er: eref (count(er, s.val) = 1
  23         => in(known, er)))
  24 */
  25
  26 # include "empset.lh"
  27
  28 # define empset_create()  (erc_create())
  29 # define empset_final(s) (erc_final(s))
  30 # define empset_member(e, s) \
  31          (!(eref_equal(_empset_get(e, s), erefNIL)))
  32 # define empset_size(es) (erc_size(es))
  33 # define empset_choose(es) (eref_get(erc_choose(es)))
  34 # define empset_sprint(es) (erc_sprint(es))
  35
  36 #define empset_elements(e, m_x) \
  37    erc_elements(e, m_y) { employee m_x = eref_get(m_y);
  38 #define end_empset_elements        } end_erc_elements
  39
  40 # endif