test/db3/empset.h

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