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