]>
Commit | Line | Data |
---|---|---|
885824d3 | 1 | imports employee; |
2 | mutable type empset; | |
3 | ||
4 | only empset empset_create(void) | |
5 | { | |
6 | /* ensures fresh(result) /\ result' = { }; */ | |
7 | } | |
8 | ||
9 | void empset_final (only empset s) | |
10 | { | |
11 | modifies s; | |
12 | /* ensures trashed(s); */ | |
13 | } | |
14 | ||
15 | void empset_clear(empset s) | |
16 | { | |
17 | modifies s; | |
18 | /* ensures s' = { }; */ | |
19 | } | |
20 | ||
21 | | bool : void | empset_insert (empset s, employee e) internalState; | |
22 | { | |
23 | modifies s, internalState; | |
24 | /* ensures result = ~(e \in s^) /\ s' = insert(e, s^); */ | |
25 | } | |
26 | ||
27 | void empset_insertUnique (empset s, employee e) internalState; | |
28 | { | |
29 | /* requires ~(e \in s^); */ | |
30 | modifies s, internalState; | |
31 | /* ensures s' = insert(e, s^); */ | |
32 | } | |
33 | ||
34 | | bool : void | empset_delete(empset s, employee e) | |
35 | { | |
36 | modifies s; | |
37 | /* ensures result = e \in s^ /\ s' = delete(e, s^); */ | |
38 | } | |
39 | ||
40 | only empset empset_union(empset s1, empset s2) internalState; | |
41 | { | |
42 | modifies internalState; | |
43 | /* ensures result' = s1^ \U s2^ /\ fresh(result); */ | |
44 | } | |
45 | ||
46 | only empset empset_disjointUnion (empset s1, empset s2) internalState; | |
47 | { | |
48 | modifies internalState; | |
49 | /* requires s1^ \I s2^ = { }; */ | |
50 | /* ensures result' = s1^ \U s2^ /\ fresh(result); */ | |
51 | } | |
52 | ||
53 | void empset_intersect (empset s1, empset s2) internalState; | |
54 | { | |
55 | modifies s1, internalState; | |
56 | /* ensures s1' = s1^ \I s2^; */ | |
57 | } | |
58 | ||
59 | int empset_size(empset s) | |
60 | { | |
61 | /* ensures result = size(s^); */ | |
62 | } | |
63 | ||
64 | bool empset_member(employee e, empset s) | |
65 | { | |
66 | /* ensures result = e \in s^; */ | |
67 | } | |
68 | ||
69 | bool empset_subset(empset s1, empset s2) | |
70 | { | |
71 | /* ensures result = s1^ \subseteq s2^; */ | |
72 | } | |
73 | ||
74 | employee empset_choose(empset s) | |
75 | { | |
76 | /* requires s^ \neq { }; */ | |
77 | /* ensures result \in s^; */ | |
78 | } | |
79 | ||
80 | only char *empset_sprint(empset s) | |
81 | { | |
82 | /* ensures isSprint(result[]', s^) /\ fresh(result[]); */ | |
83 | } | |
84 | ||
85 | void empset_initMod (void) internalState; | |
86 | { | |
87 | modifies internalState; | |
88 | ensures true; | |
89 | } | |
90 | ||
91 | iter empset_elements (empset s, yield employee x); |