diff options
| author |  rustanleino <unknown> | 2010-06-05 02:00:33 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2010-06-05 02:00:33 +0000 |
| commit | 22e67dc18705c19b617678358c8e859349938ac3 (patch) | |
| tree | 7ee7efbcb76f209c97420dbd78b049d26c2e389c /Test/dafny0/TypeParameters.dfy | |
| parent | 93ac0e1e3eb6e18895087d2420b98bd8ba06443b (diff) | |
Dafny:
* Fixed bug in translation of well-formedness conditions
* Added Test/dafny0/Celebrity.dfy
* Added a harness to Test/vacid0/Composite.dfy
Diffstat (limited to 'Test/dafny0/TypeParameters.dfy')
| -rw-r--r-- | Test/dafny0/TypeParameters.dfy | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/Test/dafny0/TypeParameters.dfy b/Test/dafny0/TypeParameters.dfy index 614c2185..e199a386 100644 --- a/Test/dafny0/TypeParameters.dfy +++ b/Test/dafny0/TypeParameters.dfy @@ -96,3 +96,19 @@ class CClient { assert z == c.x;
}
}
+
+// -------------------------
+
+static function IsCelebrity<Person>(c: Person, people: set<Person>): bool;
+ requires c == c || c in people;
+
+method FindCelebrity3(people: set<int>, ghost c: int)
+ requires IsCelebrity(c, people);
+{
+ ghost var b: bool;
+ b := IsCelebrity(c, people);
+ b := F(c, people);
+}
+
+static function F(c: int, people: set<int>): bool;
+ requires IsCelebrity(c, people);
|