home *** CD-ROM | disk | FTP | other *** search
/ OS/2 Shareware BBS: 10 Tools / 10-Tools.zip / lclint.zip / lclint-2_3h-os2-bin.zip / test / db2 / empset.h < prev    next >
C/C++ Source or Header  |  1997-09-03  |  941b  |  41 lines
  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
  41.