Merge

1 files changed, 19 insertions, 7 deletions

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