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
|
// Schorr-Waite algorithm in Chalice
// (see Test/dafny1/SchorrWaite.dfy)
// Arbitrary number of children
// Added visited field to refine non-det choice with a conditional
// Added a client
class Node {
var children: seq<Node>;
var marked: bool;
var visited: int;
ghost var path: seq<Node>;
}
class Main {
method Test()
{
var a := new Node {marked := false, visited := 0};
var b := new Node {marked := false, visited := 0};
var c := new Node {marked := false, visited := 0};
var d := new Node {marked := false, visited := 0};
a.children := [b];
b.children := [c,a];
c.children := [b];
d.children := [a,b,c];
// a <-> b <-> c
// ^ \ ^ / ^
// d
assert [a,b,c,d][0] == a; // root is in sequence
call IterativeMark(a, [a,b,c,d]);
assert a.marked;
assert a.children[0] == b; // b should be marked
assert b.marked;
assert b.children[0] == c; // c should be marked
assert c.marked;
assert !d.marked;
}
function Reachable(to: Node, p:seq<Node>, from: Node): bool
requires acc(p[*].children);
{
|p| == 0 ? to == from :
(p[0] != null && to in p[0].children && Reachable(p[0], p[1..], from))
}
method IterativeMark(root: Node, S: seq<Node>)
requires acc(S[*].*);
requires root in S;
requires forall n in S :: n != null && (forall ch in n.children :: ch != null && ch in S);
requires forall n in S :: ! n.marked;
requires forall n in S :: n.visited == 0;
ensures acc(S[*].*);
// graph structure is the same
ensures forall n in S :: n.children == old(n.children);
ensures forall n in S :: n.visited == 0;
// all nodes reachable from root are marked
ensures root.marked;
ensures forall n in S :: n.marked ==> (forall ch in n.children :: ch.marked);
// all marked nodes are reachable from root
ensures forall n in S :: n.marked ==>
(forall m in n.path :: m in S) &&
Reachable(n, n.path, root);
{
var t:Node := root;
t.marked := true;
var stack: seq<Node> := [];
t.path := stack;
var stop := false;
while(!stop)
invariant acc(S[*].*);
invariant root.marked && t in S && t.marked && t !in stack;
// no duplicates in the stack
invariant forall i in [0..|stack|] :: forall j in [i+1..|stack|] :: stack[i] != stack[j];
// stack well-formed
invariant forall n in stack :: n in S;
invariant forall n in S :: n in stack || n == t ==>
n.marked &&
0 <= n.visited && n.visited <= |n.children| &&
(forall i in [0..n.visited] :: n.children[i] in S && n.children[i].marked);
invariant forall n in stack :: n.visited < |n.children|;
// stack is linked
invariant forall i in [1..|stack|] :: stack[i-1] == stack[i].children[stack[i].visited];
invariant 0 < |stack| ==> t == stack[0].children[stack[0].visited];
// goal
invariant forall n in S :: n.marked && n !in stack && n != t ==>
(forall ch in n.children :: ch in S && ch.marked);
invariant forall n in S :: n.marked ==>
(forall m in n.path :: m in S) &&
Reachable(n, n.path, root);
// preservation
invariant forall n in S :: n !in stack && n != t ==> n.visited == old(n.visited);
invariant forall n in S :: n.children == old(n.children);
// termination
invariant stop ==> |stack| == 0 && (forall ch in t.children :: ch.marked) && t.visited == 0;
{
if (t.visited == |t.children|) {
// pop
t.visited := 0;
if (|stack| == 0) {
stop := true;
} else {
t := stack[0];
stack := stack[1..];
t.visited := t.visited + 1;
}
} else if (t.children[t.visited].marked) {
// skip
t.visited := t.visited + 1;
} else {
// push
ghost var oldt:Node := t;
stack := [t] ++ stack;
t := t.children[t.visited];
t.path := [oldt] ++ oldt.path; // TODO: in fact, this is stack
t.marked := true;
assert Reachable(oldt, oldt.path, root); // needed for limited function
}
}
}
}
|
