]>
Commit | Line | Data |
---|---|---|
885824d3 | 1 | imports employee; |
2 | ||
3 | immutable type eref; | |
4 | spec immutable type map; | |
5 | ||
6 | spec map m; | |
7 | constant eref erefNIL; | |
8 | ||
9 | eref eref_alloc(void) map m; | |
10 | { | |
11 | modifies m; | |
12 | /* ensures newInd(result, m^, m'); */ | |
13 | } | |
14 | ||
15 | void eref_free(eref er) map m; | |
16 | { | |
17 | /* requires er \in domain(m^); */ | |
18 | modifies m; | |
19 | /* ensures m' = delete(m^, er); */ | |
20 | } | |
21 | ||
22 | void eref_assign(eref er, employee e) map m; | |
23 | { | |
24 | /* requires er \in domain(m^); */ | |
25 | modifies m; | |
26 | /* ensures m' = assign(m^, er, e); */ | |
27 | } | |
28 | ||
29 | employee eref_get(eref er) map m; | |
30 | { | |
31 | /* requires er \in domain(m^); */ | |
32 | /* ensures result = m^[er]; */ | |
33 | } | |
34 | ||
35 | bool eref_equal(eref er1, eref er2) | |
36 | { | |
37 | /* ensures result = (er1 = er2); */ | |
38 | } | |
39 | ||
40 | void eref_initMod(void) map m; | |
41 | { | |
42 | modifies m; | |
43 | /* ensures m' = new; */ | |
44 | } |