diff options
| author |  rustanleino <unknown> | 2011-03-26 04:06:37 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2011-03-26 04:06:37 +0000 |
| commit | bd9003ec46d72f74c3284a63713336da630769ff (patch) | |
| tree | 9ef94aac6ff8ec9982960dec816b778f78c3d63a /Test/dafny1/Celebrity.dfy | |
| parent | dceef1d90bfc91be2ab309107d3947ce1b3667eb (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
|