diff options
| author |  rustanleino <unknown> | 2011-03-26 04:06:37 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2011-03-26 04:06:37 +0000 |
| commit | d30478027bb51b9507a31538799ca285df096bf9 (patch) | |
| tree | f16dc34816b111e95eb22de918e174f0e5b22f49 /Test/dafny1/Celebrity.dfy | |
| parent | c16176d2993c2df6b8b1b136c28a76cac3165b57 (diff) | |
Dafny: improved and corrected physical/ghost distinction
Diffstat (limited to 'Test/dafny1/Celebrity.dfy')
| -rw-r--r-- | Test/dafny1/Celebrity.dfy | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Test/dafny1/Celebrity.dfy b/Test/dafny1/Celebrity.dfy index eed06bb1..77af9327 100644 --- a/Test/dafny1/Celebrity.dfy +++ b/Test/dafny1/Celebrity.dfy @@ -4,7 +4,7 @@ method Pick<T>(S: set<T>) returns (t: T); requires S != {};
ensures t in S;
-static function Knows<Person>(a: Person, b: Person): bool;
+static function method 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
|