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
|
// Celebrity example, inspired by the Rodin tutorial
class Person
{
}
var pa: seq<Person>;
function method Knows(a: Person, b: Person): bool
reads this;
requires a != b; // forbid asking about the reflexive case
{
exists i | 0 <= i && i < |pa| :: 0 <= i < |pa| / 2 ==> pa[2*i] == a && pa[2*i+1] == b
}
function IsCelebrity(c: Person, people: set<Person>): bool
reads this;
{
c in people &&
(forall p :: p in people && p != c ==> Knows(p, c) && !Knows(c, p))
}
method FindCelebrity0(people: set<Person>, ghost c: Person) returns (r: Person)
requires (exists c :: IsCelebrity(c, people));
ensures r == c;
{
var cc; assume cc == c; // this line essentially converts ghost c to non-ghost cc
r := cc;
}
method FindCelebrity1(people: set<Person>, ghost c: Person) returns (r: Person)
requires IsCelebrity(c, people);
ensures r == c;
{
var Q := people;
var x := choose Q;
while (Q != {x})
//invariant Q <= people; // inv1 in Rodin's Celebrity_1, but it's not needed here
invariant IsCelebrity(c, Q); // inv2
invariant x in Q;
decreases Q;
{
var y := choose Q - {x};
if (Knows(x, y)) {
Q := Q - {x}; // remove_1
} else {
Q := Q - {y}; assert x in Q; // remove_2
}
x := choose Q;
}
r := x;
}
method FindCelebrity2(people: set<Person>, ghost c: Person) returns (r: Person)
requires IsCelebrity(c, people);
ensures r == c;
{
var b := choose people;
var R := people - {b};
while (R != {})
invariant R <= people; // inv1
invariant b in people; // inv2
invariant b !in R; // inv3
invariant IsCelebrity(c, R + {b}); // my non-refinement way of saying inv4
decreases R;
{
var x := choose R;
if (Knows(x, b)) {
R := R - {x};
} else {
b := x;
R := R - {x};
}
}
r := b;
}
/*
method FindCelebrity3(n: int, people: set<int>, ghost c: int) returns (r: int)
requires 0 < n;
requires (forall p :: p in people <==> 0 <= p && p < n);
requires IsCelebrity(c, people);
ensures r == c;
{
r := 0;
var a := 1;
var b := 0;
while (a < n)
invariant a <= n;
invariant b < a; // Celebrity_2/inv3 and Celebrity_3/inv2
invariant c == b || (a <= c && c < n);
{
if (Knows(a, b)) {
a := a + 1;
} else {
b := a;
a := a + 1;
}
}
r := b;
}
*/
|
