1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
|
imports eref;
mutable type erc;
only erc erc_create(void)
{
/* ensures fresh(result) /\ result' = { }; */
}
void erc_clear(erc c)
{
/* requires c^.activeIters = 0; */
modifies c;
/* ensures c' = { }; */
}
void erc_insert(erc c, eref er)
{
/* requires c^.activeIters = 0 /\ er \neq erefNIL; */
modifies c;
/* ensures c' = [insert(er, c^.val), 0]; */
}
| bool : void | erc_delete(erc c, eref er)
{
/* requires c^.activeIters = 0; */
modifies c;
/* ensures result = er \in c^.val
/\ c' = [delete(er, c^.val), 0]; */
}
bool erc_member(eref er, erc c)
{
/* ensures result = er \in c^.val; */
}
eref erc_choose(erc c)
{
/* requires size(c^.val) \neq 0; */
/* ensures result \in c^.val; */
}
int erc_size(erc c)
{
/* ensures result = size(c^.val); */
}
void erc_join(erc c1, erc c2)
{
/* requires c1^.activeIters = 0; */
modifies c1;
/* ensures c1' = [c1^.val \U c2^.val, 0]; */
}
only char *erc_sprint(erc c)
{
/* ensures isSprint(result[]', c^) /\ fresh(result[]); */
}
void erc_final (only erc c)
{
modifies c;
/* ensures trashed(c); */
}
void erc_initMod (void) internalState;
{
modifies internalState;
ensures true;
}
iter erc_elements (erc c, yield eref el);
|
