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