[splint.git] / test / db1 / empset.h

# ifndef EMPSET_H
# define EMPSET_H

# include "eref.h"
# include "erc.h"
# include "ereftab.h"

typedef erc empset;

ereftab known;

/*
  Abstraction function, toEmpSet:
    e \in toEmpSet(s) == 
      exists er (count(er, s.val) = 1
        /\ getERef(known, e) = er)

  Rep invariant:
    forall s: empset
      (forall er: eref (count(er, s.val) <= 1)
      /\ s.activeIters = 0
      /\ forall er: eref (count(er, s.val) = 1
        => in(known, er)))
*/

# include "empset.lh"

# define empset_create()  (erc_create())
# define empset_final(s) (erc_final(s))
# define empset_member(e, s) \
         (!(eref_equal(_empset_get(e, s), erefNIL)))
# define empset_size(es) (erc_size(es))
# define empset_choose(es) (eref_get(erc_choose(es)))
# define empset_sprint(es) (erc_sprint(es))

# endif
Commit	Line	Data
885824d3	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	# endif