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
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
|
// RUN: %dafny /compile:0 "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
class Composite {
var left: Composite;
var right: Composite;
var parent: Composite;
var val: int;
var sum: int;
function Valid(S: set<Composite>): bool
reads this, parent, left, right;
{
this in S &&
(parent != null ==> parent in S && (parent.left == this || parent.right == this)) &&
(left != null ==> left in S && left.parent == this && left != right) &&
(right != null ==> right in S && right.parent == this && left != right) &&
sum == val + (if left == null then 0 else left.sum) + (if right == null then 0 else right.sum)
}
function Acyclic(S: set<Composite>): bool
reads S;
{
this in S &&
(parent != null ==> parent.Acyclic(S - {this}))
}
method Init(x: int)
modifies this;
ensures Valid({this}) && Acyclic({this}) && val == x && parent == null;
{
parent := null;
left := null;
right := null;
val := x;
sum := val;
}
method Update(x: int, ghost S: set<Composite>)
requires this in S && Acyclic(S);
requires (forall c :: c in S ==> c != null && c.Valid(S));
modifies S;
ensures (forall c :: c in S ==> c.Valid(S));
ensures (forall c :: c in S ==> c.left == old(c.left) && c.right == old(c.right) && c.parent == old(c.parent));
ensures (forall c :: c in S && c != this ==> c.val == old(c.val));
ensures val == x;
{
var delta := x - val;
val := x;
Adjust(delta, S, S);
}
method Add(ghost S: set<Composite>, child: Composite, ghost U: set<Composite>)
requires this in S && Acyclic(S);
requires (forall c :: c in S ==> c != null && c.Valid(S));
requires child != null && child in U;
requires (forall c :: c in U ==> c != null && c.Valid(U));
requires S !! U;
requires left == null || right == null;
requires child.parent == null;
// modifies only one of this.left and this.right, and child.parent, and various sum fields:
modifies S, child;
ensures child.left == old(child.left) && child.right == old(child.right) && child.val == old(child.val);
ensures (forall c :: c in S && c != this ==> c.left == old(c.left) && c.right == old(c.right));
ensures old(left) != null ==> left == old(left);
ensures old(right) != null ==> right == old(right);
ensures (forall c :: c in S ==> c.parent == old(c.parent) && c.val == old(c.val));
// sets child.parent to this:
ensures child.parent == this;
// leaves everything in S+U valid:
ensures (forall c {:autotriggers false} :: c in S+U ==> c.Valid(S+U)); // We can't generate a trigger for this at the moment; if we did, we would still need to prevent TrSplitExpr from translating c in S+U to S[c] || U[c].
{
if (left == null) {
left := child;
} else {
right := child;
}
child.parent := this;
Adjust(child.sum, S, S+U);
}
method Dislodge(ghost S: set<Composite>)
requires this in S && Acyclic(S);
requires (forall c :: c in S ==> c != null && c.Valid(S));
modifies S;
ensures (forall c :: c in S ==> c.Valid(S));
ensures (forall c :: c in S ==> c.val == old(c.val));
ensures (forall c :: c in S && c != this ==> c.parent == old(c.parent));
ensures parent == null;
ensures (forall c :: c in S ==> c.left == old(c.left) || (old(c.left) == this && c.left == null));
ensures (forall c :: c in S ==> c.right == old(c.right) || (old(c.right) == this && c.right == null));
ensures Acyclic({this});
{
var p := parent;
parent := null;
if (p != null) {
if (p.left == this) {
p.left := null;
} else {
p.right := null;
}
var delta := -sum;
p.Adjust(delta, S - {this}, S);
}
}
/*private*/ method Adjust(delta: int, ghost U: set<Composite>, ghost S: set<Composite>)
requires U <= S && Acyclic(U);
// everything else is valid:
requires (forall c :: c in S && c != this ==> c != null && c.Valid(S));
// this is almost valid:
requires parent != null ==> parent in S && (parent.left == this || parent.right == this);
requires left != null ==> left in S && left.parent == this && left != right;
requires right != null ==> right in S && right.parent == this && left != right;
// ... except that sum needs to be adjusted by delta:
requires sum + delta == val + (if left == null then 0 else left.sum) + (if right == null then 0 else right.sum);
// modifies sum fields in U:
modifies U`sum;
// everything is valid, including this:
ensures (forall c :: c in S ==> c.Valid(S));
{
var p := this;
ghost var T := U;
while (p != null)
invariant T <= U;
invariant p == null || p.Acyclic(T);
invariant (forall c :: c in S && c != p ==> c.Valid(S));
invariant p != null ==> p.sum + delta == p.val + (if p.left == null then 0 else p.left.sum) + (if p.right == null then 0 else p.right.sum);
invariant (forall c :: c in S ==> c.left == old(c.left) && c.right == old(c.right) && c.parent == old(c.parent) && c.val == old(c.val));
decreases T;
{
p.sum := p.sum + delta;
T := T - {p};
p := p.parent;
}
}
}
method Main()
{
var c0 := new Composite.Init(57);
var c1 := new Composite.Init(12);
c0.Add({c0}, c1, {c1});
var c2 := new Composite.Init(48);
var c3 := new Composite.Init(48);
c2.Add({c2}, c3, {c3});
c0.Add({c0,c1}, c2, {c2,c3});
ghost var S := {c0, c1, c2, c3};
c1.Update(100, S);
c2.Update(102, S);
c2.Dislodge(S);
c2.Update(496, S);
c0.Update(0, S);
}
method Harness() {
var a := new Composite.Init(5);
var b := new Composite.Init(7);
a.Add({a}, b, {b});
assert a.sum == 12;
b.Update(17, {a,b});
assert a.sum == 22;
var c := new Composite.Init(10);
b.Add({a,b}, c, {c});
b.Dislodge({a,b,c});
assert b.sum == 27;
}
|
