diff options
| author |  rustanleino <unknown> | 2010-06-08 18:05:23 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2010-06-08 18:05:23 +0000 |
| commit | 2e8f477b81b1c5c6d3c3f600abac3874548a9e4d (patch) | |
| tree | 03e89bdb4df3a689b7217c5e913557c5b6c6df99 /Test/dafny1/Celebrity.dfy | |
| parent | 22e67dc18705c19b617678358c8e859349938ac3 (diff) | |
Boogie:
* Look for Z3 versions up to 2.15 (but did not implement a better algorithm for it).
* Added prover-path output as part of /trace flag (that probably isn't the best command-line option for it).
Dafny:
* Split off some tests from Test/dafny0 into Test/dafny1.
* Added Test/dafny1/UltraFilter.dfy.
Diffstat (limited to 'Test/dafny1/Celebrity.dfy')
| -rw-r--r-- | Test/dafny1/Celebrity.dfy | 95 |
1 files changed, 95 insertions, 0 deletions
diff --git a/Test/dafny1/Celebrity.dfy b/Test/dafny1/Celebrity.dfy new file mode 100644 index 00000000..fd267c71 --- /dev/null +++ b/Test/dafny1/Celebrity.dfy @@ -0,0 +1,95 @@ +// Celebrity example, inspired by the Rodin tutorial
+
+method Pick<T>(S: set<T>) returns (t: T);
+ requires S != {};
+ ensures t in S;
+
+static function Knows<Person>(a: Person, b: Person): bool;
+ requires a != b; // forbid asking about the reflexive case
+
+static function IsCelebrity<Person>(c: Person, people: set<Person>): bool
+{
+ c in people &&
+ (forall p :: p in people && p != c ==> Knows(p, c) && !Knows(c, p))
+}
+
+method FindCelebrity0<Person>(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<Person>(people: set<Person>, ghost c: Person) returns (r: Person)
+ requires IsCelebrity(c, people);
+ ensures r == c;
+{
+ var Q := people;
+ call x := Pick(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;
+ {
+ call y := Pick(Q - {x});
+ if (Knows(x, y)) {
+ Q := Q - {x}; // remove_1
+ } else {
+ Q := Q - {y}; assert x in Q; // remove_2
+ }
+ call x := Pick(Q);
+ }
+ r := x;
+}
+
+method FindCelebrity2<Person>(people: set<Person>, ghost c: Person) returns (r: Person)
+ requires IsCelebrity(c, people);
+ ensures r == c;
+{
+ call b := Pick(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;
+ {
+ call x := Pick(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); // see next line:
+ requires c in people && (forall p :: p in people && p != c ==> Knows(p, c) && !Knows(c, p)); // hack to work around bug in Dafny-to-Boogie translator
+ 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;
+}
|