blob: b0d398e054d4fad55f46f859661b62ddb71681f0 (
plain)
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
|
// Celebrity example, inspired by the Rodin tutorial
class Person {
function knows(other: Person): bool
requires this != other;
}
class Celebrity0 {
function IsCelebrity(c: Person, people: seq<Person>): bool
requires null !in people;
{
c in people && forall p in people :: p != c ==> (p.knows(c)) && (! c.knows(p))
}
method Find(people: seq<Person>, /*ghost*/ c: Person) returns (r: Person)
requires null !in people && IsCelebrity(c, people);
{
var r [r == c];
}
}
/** Without theory of sets, hard to describe: "remove an element from a sequence" */
class Celebrity1 refines Celebrity0 {
refines Find(people: seq<Person>, c: Person) returns (r: Person)
{
var q:seq<Person> := people;
// pick and remove a
var a:Person := q[0]; q := q[1..]; assert people == [a] ++ q;
while (|q| > 0)
invariant forall p in q :: p in people;
invariant a in people;
invariant IsCelebrity(c,[a] ++ q);
{
// pick and remove b
var oldq:seq<Person> := q;
var b:Person := q[0]; q := q[1..];
assert oldq == [b] ++ q;
if (a != b && a.knows(b)) {
a := b;
}
}
r := a;
}
}
|
