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/dafny0/SmallTests.dfy | |
| 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/dafny0/SmallTests.dfy')
| -rw-r--r-- | Test/dafny0/SmallTests.dfy | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy index e8b618d7..40df1135 100644 --- a/Test/dafny0/SmallTests.dfy +++ b/Test/dafny0/SmallTests.dfy @@ -294,7 +294,7 @@ method QuantifierRange1<T>(a: seq<T>, x: T, y: T, N: int) assert x != y;
}
-method QuantifierRange2<T>(a: seq<T>, x: T, y: T, N: int)
+method QuantifierRange2<T(==)>(a: seq<T>, x: T, y: T, N: int)
requires 0 <= N && N <= |a|;
requires exists k | 0 <= k && k < N :: a[k] == y;
ensures forall k | 0 <= k && k < N :: a[k] == y; // error
|