]>
Commit | Line | Data |
---|---|---|
885824d3 | 1 | imports eref; |
2 | ||
3 | mutable type erc; | |
4 | ||
5 | erc erc_create(void) | |
6 | { | |
7 | /* ensures fresh(result) /\ result' = { }; */ | |
8 | } | |
9 | ||
10 | void erc_clear(erc c) | |
11 | { | |
12 | /* requires c^.activeIters = 0; */ | |
13 | modifies c; | |
14 | /* ensures c' = { }; */ | |
15 | } | |
16 | ||
17 | void erc_insert(erc c, eref er) | |
18 | { | |
19 | /* requires c^.activeIters = 0 /\ er \neq erefNIL; */ | |
20 | modifies c; | |
21 | /* ensures c' = [insert(er, c^.val), 0]; */ | |
22 | } | |
23 | ||
24 | | bool : void | erc_delete(erc c, eref er) | |
25 | { | |
26 | /* requires c^.activeIters = 0; */ | |
27 | modifies c; | |
28 | /* ensures result = er \in c^.val | |
29 | /\ c' = [delete(er, c^.val), 0]; */ | |
30 | } | |
31 | ||
32 | bool erc_member(eref er, erc c) | |
33 | { | |
34 | /* ensures result = er \in c^.val; */ | |
35 | } | |
36 | ||
37 | eref erc_choose(erc c) | |
38 | { | |
39 | /* requires size(c^.val) \neq 0; */ | |
40 | /* ensures result \in c^.val; */ | |
41 | } | |
42 | ||
43 | int erc_size(erc c) | |
44 | { | |
45 | /* ensures result = size(c^.val); */ | |
46 | } | |
47 | ||
48 | void erc_join(erc c1, erc c2) | |
49 | { | |
50 | /* requires c1^.activeIters = 0; */ | |
51 | modifies c1; | |
52 | /* ensures c1' = [c1^.val \U c2^.val, 0]; */ | |
53 | } | |
54 | ||
55 | char *erc_sprint(erc c) | |
56 | { | |
57 | /* ensures isSprint(result[]', c^) /\ fresh(result[]); */ | |
58 | } | |
59 | ||
60 | void erc_final(erc c) | |
61 | { | |
62 | modifies c; | |
63 | /* ensures trashed(c); */ | |
64 | } | |
65 | ||
66 | void erc_initMod(void) | |
67 | { | |
68 | modifies internalState; | |
69 | ensures true; | |
70 | } | |
71 | ||
72 | iter erc_elements (erc c, yield eref el); |