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