From 47c23bd0d7e71722a94b8df660c0314381b4263a Mon Sep 17 00:00:00 2001
From: Jason Koenig <unknown>
Date: Fri, 15 Jul 2011 17:42:55 -0700
Subject: Fixed regression test failures due to removal of bodiless methods and
 functions.

---
 Test/dafny1/Celebrity.dfy | 26 +++++++++++++++++++-------
 1 file changed, 19 insertions(+), 7 deletions(-)

(limited to 'Test/dafny1/Celebrity.dfy')

diff --git a/Test/dafny1/Celebrity.dfy b/Test/dafny1/Celebrity.dfy
index 21b895aa..a10c4324 100644
--- a/Test/dafny1/Celebrity.dfy
+++ b/Test/dafny1/Celebrity.dfy
@@ -1,15 +1,26 @@
 // Celebrity example, inspired by the Rodin tutorial
 
-static function method Knows<Person>(a: Person, b: Person): bool
-  requires a != b;  // forbid asking about the reflexive case
+class Person
+{
+
+}
+
+var pa: seq<Person>;
 
-static function IsCelebrity<Person>(c: Person, people: set<Person>): bool
+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<Person>(people: set<Person>, ghost c: Person) returns (r: Person)
+method FindCelebrity0(people: set<Person>, ghost c: Person) returns (r: Person)
   requires (exists c :: IsCelebrity(c, people));
   ensures r == c;
 {
@@ -17,7 +28,7 @@ method FindCelebrity0<Person>(people: set<Person>, ghost c: Person) returns (r:
   r := cc;
 }
 
-method FindCelebrity1<Person>(people: set<Person>, ghost c: Person) returns (r: Person)
+method FindCelebrity1(people: set<Person>, ghost c: Person) returns (r: Person)
   requires IsCelebrity(c, people);
   ensures r == c;
 {
@@ -40,7 +51,7 @@ method FindCelebrity1<Person>(people: set<Person>, ghost c: Person) returns (r:
   r := x;
 }
 
-method FindCelebrity2<Person>(people: set<Person>, ghost c: Person) returns (r: Person)
+method FindCelebrity2(people: set<Person>, ghost c: Person) returns (r: Person)
   requires IsCelebrity(c, people);
   ensures r == c;
 {
@@ -64,7 +75,7 @@ method FindCelebrity2<Person>(people: set<Person>, ghost c: Person) returns (r:
   }
   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);
@@ -88,3 +99,4 @@ method FindCelebrity3(n: int, people: set<int>, ghost c: int) returns (r: int)
   }
   r := b;
 }
+*/
\ No newline at end of file
-- 
cgit v1.2.3