]>
Commit | Line | Data |
---|---|---|
885824d3 | 1 | imports eref; |
2 | ||
3 | mutable type erc; | |
4 | mutable type ercIter; | |
5 | ||
6 | erc erc_create(void) | |
7 | { | |
8 | /* ensures fresh(result) /\ result' = { }; */ | |
9 | } | |
10 | ||
11 | void erc_clear(erc c) | |
12 | { | |
13 | /* requires c^.activeIters = 0; */ | |
14 | modifies c; | |
15 | /* ensures c' = { }; */ | |
16 | } | |
17 | ||
18 | void erc_insert(erc c, eref er) | |
19 | { | |
20 | /* requires c^.activeIters = 0 /\ er \neq erefNIL; */ | |
21 | modifies c; | |
22 | /* ensures c' = [insert(er, c^.val), 0]; */ | |
23 | } | |
24 | ||
25 | bool erc_delete(erc c, eref er) | |
26 | { | |
27 | /* requires c^.activeIters = 0; */ | |
28 | modifies c; | |
29 | /* ensures result = er \in c^.val | |
30 | /\ c' = [delete(er, c^.val), 0]; */ | |
31 | } | |
32 | ||
33 | bool erc_member(eref er, erc c) | |
34 | { | |
35 | /* ensures result = er \in c^.val; */ | |
36 | } | |
37 | ||
38 | eref erc_choose(erc c) | |
39 | { | |
40 | /* requires size(c^.val) \neq 0; */ | |
41 | /* ensures result \in c^.val; */ | |
42 | } | |
43 | ||
44 | int erc_size(erc c) | |
45 | { | |
46 | /* ensures result = size(c^.val); */ | |
47 | } | |
48 | ||
49 | ercIter erc_iterStart(erc c) | |
50 | { | |
51 | modifies c; | |
52 | /* ensures fresh(result) /\ result' = [c^.val, c] | |
53 | /\ c' = startIter(c^); | |
54 | */ | |
55 | } | |
56 | ||
57 | eref erc_yield(ercIter it) | |
58 | { | |
59 | modifies it; /* , it^.eObj */ | |
60 | /* ensures if it^.toYield \neq { } | |
61 | then yielded(result, it^, it') | |
62 | /\ (it^.eObj)' = (it^.eObj)^ | |
63 | else result = erefNIL /\ trashed(it) | |
64 | /\ (it^.eObj)' = endIter((it^.eObj)^); | |
65 | */ | |
66 | } | |
67 | ||
68 | void erc_iterFinal(ercIter it) | |
69 | { | |
70 | modifies it; /* , it^.eObj; */ | |
71 | /* ensures trashed(it) | |
72 | /\ (it^.eObj)' = endIter((it^.eObj)^); | |
73 | */ | |
74 | } | |
75 | ||
76 | void erc_join(erc c1, erc c2) | |
77 | { | |
78 | /* requires c1^.activeIters = 0; */ | |
79 | modifies c1; | |
80 | /* ensures c1' = [c1^.val \U c2^.val, 0]; */ | |
81 | } | |
82 | ||
83 | char *erc_sprint(erc c) | |
84 | { | |
85 | /* ensures isSprint(result[]', c^) /\ fresh(result[]); */ | |
86 | } | |
87 | ||
88 | void erc_final(erc c) | |
89 | { | |
90 | modifies c; | |
91 | /* ensures trashed(c); */ | |
92 | } | |
93 | ||
94 | void erc_initMod(void) | |
95 | { | |
96 | ensures true; | |
97 | } |