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
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
|
imports eref;
mutable type erc;
mutable type ercIter;
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 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); */
}
ercIter erc_iterStart(erc c)
{
modifies c;
/* ensures fresh(result) /\ result' = [c^.val, c]
/\ c' = startIter(c^);
*/
}
eref erc_yield(ercIter it)
{
modifies it; /* , it^.eObj */
/* ensures if it^.toYield \neq { }
then yielded(result, it^, it')
/\ (it^.eObj)' = (it^.eObj)^
else result = erefNIL /\ trashed(it)
/\ (it^.eObj)' = endIter((it^.eObj)^);
*/
}
void erc_iterFinal(ercIter it)
{
modifies it; /* , it^.eObj; */
/* ensures trashed(it)
/\ (it^.eObj)' = endIter((it^.eObj)^);
*/
}
void erc_join(erc c1, erc c2)
{
/* requires c1^.activeIters = 0; */
modifies c1;
/* ensures c1' = [c1^.val \U c2^.val, 0]; */
}
char *erc_sprint(erc c)
{
/* ensures isSprint(result[]', c^) /\ fresh(result[]); */
}
void erc_final(erc c)
{
modifies c;
/* ensures trashed(c); */
}
void erc_initMod(void)
{
ensures true;
}
|
