diff options
| author |  Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-06-21 19:16:05 -0700 |
|---|---|---|
| committer | Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-06-21 19:16:05 -0700 |
| commit | 7c6cfaa37c96349fda99823c6f98a576dba194b4 (patch) | |
| tree | 0305efde49467759af3cce939c9a1ce70ad0cd61 /Test/dafny1 | |
| parent | 1ba9b5fab7fff5c30be347e84ff3cf348ec9857d (diff) | |
Dafny: Since it's no longer true that all types support equality at run-time (in particular, codatatypes), Dafny needs to check this. In these changes, Dafny supports the "(==)" suffix to type parameters, infers that suffix in some cases, and enforces equality support in many places. Refinement and datatypes still need more attention in the Dafny implementation.
Diffstat (limited to 'Test/dafny1')
| -rw-r--r-- | Test/dafny1/Celebrity.dfy | 2 | ||||
| -rw-r--r-- | Test/dafny1/UltraFilter.dfy | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/Test/dafny1/Celebrity.dfy b/Test/dafny1/Celebrity.dfy index 21b895aa..4c761671 100644 --- a/Test/dafny1/Celebrity.dfy +++ b/Test/dafny1/Celebrity.dfy @@ -10,7 +10,7 @@ static function IsCelebrity<Person>(c: Person, people: set<Person>): bool }
method FindCelebrity0<Person>(people: set<Person>, ghost c: Person) returns (r: Person)
- requires (exists c :: IsCelebrity(c, people));
+ requires exists c :: IsCelebrity(c, people);
ensures r == c;
{
var cc; assume cc == c; // this line essentially converts ghost c to non-ghost cc
diff --git a/Test/dafny1/UltraFilter.dfy b/Test/dafny1/UltraFilter.dfy index c8419890..c78d5e81 100644 --- a/Test/dafny1/UltraFilter.dfy +++ b/Test/dafny1/UltraFilter.dfy @@ -1,6 +1,6 @@ // ultra filter
-class UltraFilter<G> {
+class UltraFilter<G(==)> {
static function IsFilter(f: set<set<G>>, S: set<G>): bool
{
(forall A, B :: A in f && A <= B ==> B in f) &&
|