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
|
// Schorr-Waite algorithm in Chalice
// (see Test/dafny1/SchorrWaite.dfy)
// (incomplete version) Two children instead of a sequence of an array
class Node {
var left: Node;
var right: Node;
var marked: bool;
var l: bool;
var r: bool;
}
class Main {
method RecursiveMark(root: Node, S: seq<Node>)
requires acc(S[*].marked, 50) && acc(S[*].*, 50);
requires root != null && root in S;
// S is closed under 'left' and 'right':
requires forall n in S :: n != null &&
((n.left != null ==> n.left in S) &&
(n.right != null ==> n.right in S));
requires forall n in S :: ! n.marked;
ensures acc(S[*].marked, 50) && acc(S[*].*, 50);
ensures root.marked;
// nodes reachable from 'root' are marked:
ensures forall n in S :: n.marked ==>
((n.left != null ==> n.left in S && n.left.marked) &&
(n.right != null ==> n.right in S && n.right.marked));
{
var stack: seq<Node> := [];
call RecursiveMarkWorker(root, S, stack);
}
method RecursiveMarkWorker(root: Node, S: seq<Node>, stack: seq<Node>)
requires acc(S[*].marked, 50) && acc(S[*].*, 50);
requires root != null && root in S;
requires forall n in S :: n != null &&
((n.left != null ==> n.left in S) &&
(n.right != null ==> n.right in S))
requires forall n in S :: n.marked ==>
(n in stack ||
((n.left != null ==> n.left.marked) &&
(n.right != null ==> n.right.marked)));
requires forall n in stack :: n != null && n in S && n.marked;
ensures acc(S[*].marked, 50) && acc(S[*].*, 50);
ensures forall n in S :: n.left == old(n.left) && n.right == old(n.right);
ensures forall n in S :: n.marked ==>
(n in stack ||
((n.left != null ==> n.left.marked) &&
(n.right != null ==> n.right.marked)));
ensures forall n in S :: old(n.marked) ==> n.marked;
ensures root.marked;
{
if (! root.marked) {
root.marked := true;
var next:seq<Node> := [root] ++ stack;
assert next[0] == root;
if (root.left != null) {
call RecursiveMarkWorker(root.left, S, next);
}
if (root.right != null) {
call RecursiveMarkWorker(root.right, S, next);
}
}
}
method IterativeMark(root: Node, S: seq<Node>)
requires acc(S[*].*);
requires root in S;
requires forall n in S :: n != null &&
(n.left != null ==> n.left in S) &&
(n.right != null ==> n.right in S);
requires forall n in S :: ! n.marked;
requires forall n in S :: ! n.l && ! n.r;
ensures acc(S[*].*);
ensures forall n in S :: n.left == old(n.left) && n.right == old(n.right);
ensures root.marked;
ensures forall n in S :: n.marked ==>
(n.left != null ==> n.left.marked) &&
(n.right != null ==> n.right.marked);
ensures forall n in S :: ! n.l && ! n.r;
{
var t:Node := root;
t.marked := true;
var stack: seq<Node> := [];
var stop := false;
while(!stop)
invariant acc(S[*].*);
invariant root.marked && t in S && t !in stack;
invariant forall n in stack :: n in S;
invariant forall i in [0..|stack|] :: forall j in [i+1..|stack|] :: stack[i] != stack[j];
invariant forall n in S :: (n in stack || n == t) ==>
n.marked &&
(n.r ==> n.l) &&
(n.l && n.left != null ==> n.left in S && n.left.marked) &&
(n.r && n.right != null ==> n.right in S && n.right.marked)
// stack is linked
invariant forall i in [1..|stack|] :: stack[i-1] == (stack[i].l ? stack[i].right : stack[i].left);
invariant 0 < |stack| ==> t == (stack[0].l ? stack[0].right : stack[0].left);
// goal
invariant forall n in S :: n.marked && n !in stack && n != t ==>
(n.left != null ==> n.left in S && n.left.marked) &&
(n.right != null ==> n.right in S && n.right.marked);
// preservation
invariant forall n in S :: n !in stack && n != t ==> ! n.l && ! n.r;
invariant forall n in S :: n.left == old(n.left) && n.right == old(n.right);
invariant stop ==> |stack| == 0 && ! t.l && ! t.r &&
(t.left != null ==> t.left.marked) &&
(t.right != null ==> t.right.marked);
{
if (! t.l && (t.left == null || t.left.marked)) {
// advance
t.l := true;
} else if (t.l && ! t.r && (t.right == null || t.right.marked)) {
// advance
t.r := true;
} else if (t.r) {
// pop
t.l := false;
t.r := false;
if (|stack| == 0) {
stop := true;
} else {
t := stack[0];
stack := stack[1..];
if (t.l) {t.r := true} else {t.l := true}
}
} else if (!t.l) {
// push
stack := [t] ++ stack;
assert stack[0] == t;
t := t.left;
t.marked := true;
} else if (!t.r) {
// push
assert t.l;
stack := [t] ++ stack;
assert stack[0] == t;
t := t.right;
t.marked := true;
}
}
}
}
|
