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 / db3 / empset.h < prev    next >
C/C++ Source or Header  |  1997-09-03  |  841b  |  37 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. /*
  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
  37.