diff options
| author |  Rustan Leino <leino@microsoft.com> | 2012-06-22 20:56:23 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2012-06-22 20:56:23 -0700 |
| commit | 5d7c99ee7733108b73d3f26cacc2f7480baea22a (patch) | |
| tree | dd2f726058cfc71630f3019c48b8630a24da5368 /Test | |
| parent | da2009988989d01acb0fc523fb533853f05f193c (diff) | |
Dafny: now, equality-support determination and checking feels ripe; so, codatatypes would then be sound
Dafny: added special case to allow equality comparison against parameter-less datatype values
Diffstat (limited to 'Test')
| -rw-r--r-- | Test/dafny0/Answer | 6 | ||||
| -rw-r--r-- | Test/dafny0/EqualityTypes.dfy | 6 | ||||
| -rw-r--r-- | Test/dafny0/Termination.dfy | 4 |
3 files changed, 10 insertions, 6 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index cd30fea6..7510363a 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -1329,10 +1329,14 @@ Dafny program verifier finished with 12 verified, 0 errors -------------------- EqualityTypes.dfy --------------------
EqualityTypes.dfy(31,13): Error: a type declaration that requires equality support cannot be replaced by a codatatype
+EqualityTypes.dfy(32,11): Error: datatype 'Y' is used to refine an arbitrary type with equality support, but 'Y' does not support equality
EqualityTypes.dfy(37,11): Error: arbitrary type 'X' is not allowed to be replaced by a datatype that takes type parameters
EqualityTypes.dfy(38,8): Error: arbitrary type 'Y' is not allowed to be replaced by a class that takes type parameters
+EqualityTypes.dfy(42,11): Error: datatype 'X' is used to refine an arbitrary type with equality support, but 'X' does not support equality
+EqualityTypes.dfy(43,11): Error: datatype 'Y' is used to refine an arbitrary type with equality support, but 'Y' does not support equality
+EqualityTypes.dfy(63,7): Error: == can only be applied to expressions of types that support equality (got Dt<T>)
EqualityTypes.dfy(82,8): Error: type parameter 0 (T) passed to method M must support equality (got _T0)
-4 resolution/type errors detected in EqualityTypes.dfy
+8 resolution/type errors detected in EqualityTypes.dfy
-------------------- SplitExpr.dfy --------------------
diff --git a/Test/dafny0/EqualityTypes.dfy b/Test/dafny0/EqualityTypes.dfy index bbcb988f..251b2e2f 100644 --- a/Test/dafny0/EqualityTypes.dfy +++ b/Test/dafny0/EqualityTypes.dfy @@ -57,11 +57,11 @@ module H { method M<T(==)>(x: T)
{ }
- function F<T>(x: BulkyList<T>, y: BulkyList<T>): int
+ function method F<T>(x: BulkyList<T>, y: BulkyList<T>): int
{ if x == y then 5 else 7 } // this equality is allowed
- function G<T>(x: Dt<T>, y: Dt<T>): int
+ function method G<T>(x: Dt<T>, y: Dt<T>): int
{ if x == y then 5 else 7 } // error: the equality is not allowed, because Dt<T> may not support equality
- function G'<T(==)>(x: Dt<T>, y: Dt<T>): int
+ function method G'<T(==)>(x: Dt<T>, y: Dt<T>): int
{ if x == y then 5 else 7 } // fine
method Caller0(b: BulkyList, y: int) {
diff --git a/Test/dafny0/Termination.dfy b/Test/dafny0/Termination.dfy index 1482dc24..bf3702ae 100644 --- a/Test/dafny0/Termination.dfy +++ b/Test/dafny0/Termination.dfy @@ -92,8 +92,8 @@ class Termination { ensures a == List.Cons(val, b);
{
match a {
- case Cons(v, r) => val := v; b := r;
- }
+ case Cons(v, r) => val := v; b := r;
+ }
}
}
|