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
|
// Celebrity example, inspired by the Rodin tutorial
class Person {
var knows: seq<Person>;
}
class Celebrity {
function IsCelebrity(c: Person, people: seq<Person>): bool
requires forall p in people :: p != null;
requires c in people && rd(people[*].knows);
{
forall p in people :: p != c ==> (c in p.knows) && (p !in c.knows)
}
method FindCelebrity0(people: seq<Person>) returns (r: Person)
requires null !in people && rd(people[*].knows);
requires exists c in people :: IsCelebrity(c, people);
ensures rd(people[*].knows);
ensures r in people && IsCelebrity(r, people);
{
var cc:Person;
assume cc in people && IsCelebrity(cc, people);
r := cc;
}
method FindCelebrity1(people: seq<Person>) returns (r: Person)
requires null !in people && rd(people[*].knows);
requires exists c in people :: IsCelebrity(c, people);
ensures rd(people[*].knows);
ensures r in people && IsCelebrity(r, people);
{
call r := Eliminate0(people, people);
}
method Eliminate0(Q: seq<Person>, people: seq<Person>) returns (r: Person)
requires null !in people && rd(people[*].knows);
requires forall c in Q :: c != null && c in people;
requires exists c in Q :: IsCelebrity(c, people);
ensures rd(people[*].knows);
ensures r in people && IsCelebrity(r, people);
{
if (|Q| == 1) {
r := Q[0];
} else {
var x:Person := Q[0];
var y:Person := Q[1];
var W:seq<Person>;
assume x != y;
if (y in x.knows) {
W := Q[1..];
assert !IsCelebrity(x, people);
assert Q == [x] ++ W;
} else {
W := [x] ++ Q[2..];
assert !IsCelebrity(y, people);
assert W[0] == x;
assert W[1..] == Q[2..];
assert exists c in W :: IsCelebrity(c, people);
}
call r := Eliminate0(W, people);
}
}
}
|
