diff options
author | Rustan Leino <unknown> | 2015-07-02 16:06:02 -0700 |
---|---|---|
committer | Rustan Leino <unknown> | 2015-07-02 16:06:02 -0700 |
commit | e10098cde7bac9a7a1576000fa29d15f1fcd8970 (patch) | |
tree | 424cc0d382c4f870fa133c18228809da4d6a1bea /Test/dafny0 | |
parent | c7f6887e452cbb91a8297bb64db39a8066750351 (diff) |
Type parameters in method/function signatures are no longer auto-declared. Although
convenient and concise, the auto-declare behavior has on many occasions caused
confusion when a type name has accidentally been mistyped (and Dafny had then
accepted and auto-declared the name).
Note, the behavior of filling in missing type parameters is still supported. This
mode, although unusual (even original?) in languages, is different from the auto-
declare behavior. For auto-declare, identifiers could be used in the program
without having a declaration. For fill-in parameters, the implicitly declared
type parameters remain anonymous.
Diffstat (limited to 'Test/dafny0')
-rw-r--r-- | Test/dafny0/Basics.dfy | 2 | ||||
-rw-r--r-- | Test/dafny0/Modules0.dfy | 14 | ||||
-rw-r--r-- | Test/dafny0/Modules0.dfy.expect | 19 | ||||
-rw-r--r-- | Test/dafny0/NestedMatch.dfy | 2 | ||||
-rw-r--r-- | Test/dafny0/NestedPatterns.dfy | 8 | ||||
-rw-r--r-- | Test/dafny0/ResolutionErrors.dfy | 10 |
6 files changed, 22 insertions, 33 deletions
diff --git a/Test/dafny0/Basics.dfy b/Test/dafny0/Basics.dfy index c8fa76c8..89b0f02a 100644 --- a/Test/dafny0/Basics.dfy +++ b/Test/dafny0/Basics.dfy @@ -100,7 +100,7 @@ method ExpliesAssociativityM(A: bool, B: bool, C: bool) { }
}
-method ExpliesShortCircuiting(a: array<T>)
+method ExpliesShortCircuiting(a: array)
{
assert a == null || 0 <= a.Length; // (W)
assert a != null ==> 0 <= a.Length; // (X) -- same as (W)
diff --git a/Test/dafny0/Modules0.dfy b/Test/dafny0/Modules0.dfy index 34aba3de..dbbffd87 100644 --- a/Test/dafny0/Modules0.dfy +++ b/Test/dafny0/Modules0.dfy @@ -71,16 +71,17 @@ module X1 { }
module X2 {
+ import opened X1
class MyClass2 {
- method Down(x1: MyClass1, x0: MyClass0) {
+ method Down(x1: MyClass1, x0: X0'.MyClass0) {
x1.Down(x0);
}
- method WayDown(x0: MyClass0) {
+ method WayDown(x0: X0'.MyClass0) {
x0.Down();
}
method Up() {
}
- method Somewhere(y: MyClassY) {
+ method Somewhere(y: MyClassY) { // error: no such type in scope
y.M();
}
}
@@ -97,8 +98,7 @@ module YY { class ClassG {
method T() { }
function method TFunc(): int { 10 }
- method V(y: MyClassY) { // Note, MyClassY is in scope, since we are in the _default
- // module, which imports everything
+ method V(y: MyClassY) {
y.M();
}
}
@@ -141,10 +141,10 @@ class AClassWithSomeField { SomeField := SomeField + 4;
var a := old(SomeField); // error: old can only be used in ghost contexts
var b := fresh(this); // error: fresh can only be used in ghost contexts
- var c := allocated(this); // error: allocated can only be used in ghost contexts
+// var c := allocated(this); // error: allocated can only be used in ghost contexts
if (fresh(this)) { // this guard makes the if statement a ghost statement
ghost var x := old(SomeField); // this is a ghost context, so it's okay
- ghost var y := allocated(this); // this is a ghost context, so it's okay
+// ghost var y := allocated(this); // this is a ghost context, so it's okay
}
}
}
diff --git a/Test/dafny0/Modules0.dfy.expect b/Test/dafny0/Modules0.dfy.expect index 5d11f9c9..d2f0bcc8 100644 --- a/Test/dafny0/Modules0.dfy.expect +++ b/Test/dafny0/Modules0.dfy.expect @@ -9,13 +9,8 @@ Modules0.dfy(15,11): Error: Duplicate name of top-level declaration: WazzupB Modules0.dfy(56,21): Error: Undeclared top-level type or type parameter: MyClass1 (did you forget to qualify a name?)
Modules0.dfy(57,21): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget to qualify a name?)
Modules0.dfy(68,21): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget to qualify a name?)
-Modules0.dfy(76,9): Error: type MyClass1 does not have a member Down
-Modules0.dfy(76,13): Error: expected method call, found expression
-Modules0.dfy(79,9): Error: type MyClass0 does not have a member Down
-Modules0.dfy(79,13): Error: expected method call, found expression
-Modules0.dfy(84,8): Error: type MyClassY does not have a member M
-Modules0.dfy(84,9): Error: expected method call, found expression
-Modules0.dfy(92,19): Error: Undeclared top-level type or type parameter: ClassG (did you forget to qualify a name?)
+Modules0.dfy(84,24): Error: Undeclared top-level type or type parameter: MyClassY (did you forget to qualify a name?)
+Modules0.dfy(93,19): Error: Undeclared top-level type or type parameter: ClassG (did you forget to qualify a name?)
Modules0.dfy(226,15): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name?)
Modules0.dfy(226,8): Error: new can be applied only to reference types (got X)
Modules0.dfy(235,13): Error: module 'B' does not declare a type 'X'
@@ -35,11 +30,5 @@ Modules0.dfy(320,11): Error: Undeclared top-level type or type parameter: Wazzup Modules0.dfy(321,17): Error: module 'Q_Imp' does not declare a type 'Edon'
Modules0.dfy(323,10): Error: new can be applied only to reference types (got Q_Imp.List<?>)
Modules0.dfy(324,30): Error: member Create does not exist in class Klassy
-Modules0.dfy(102,6): Error: type MyClassY does not have a member M
-Modules0.dfy(102,7): Error: expected method call, found expression
-Modules0.dfy(127,11): Error: ghost variables are allowed only in specification contexts
-Modules0.dfy(142,13): Error: old expressions are allowed only in specification and ghost contexts
-Modules0.dfy(143,13): Error: fresh expressions are allowed only in specification and ghost contexts
-Modules0.dfy(144,13): Error: unresolved identifier: allocated
-Modules0.dfy(147,21): Error: unresolved identifier: allocated
-42 resolution/type errors detected in Modules0.dfy
+Modules0.dfy(101,14): Error: Undeclared top-level type or type parameter: MyClassY (did you forget to qualify a name?)
+31 resolution/type errors detected in Modules0.dfy
diff --git a/Test/dafny0/NestedMatch.dfy b/Test/dafny0/NestedMatch.dfy index e6e7c489..81319b4a 100644 --- a/Test/dafny0/NestedMatch.dfy +++ b/Test/dafny0/NestedMatch.dfy @@ -28,7 +28,7 @@ function last<T>(xs: List<T>): T case Cons(y, Cons(z, zs)) => last(Cons(z, zs))
}
-method checkLast(y: T) {
+method checkLast<T>(y: T) {
assert last(Cons(y, Nil)) == y;
assert last(Cons(y, Cons(y, Nil))) == last(Cons(y, Nil));
}
diff --git a/Test/dafny0/NestedPatterns.dfy b/Test/dafny0/NestedPatterns.dfy index ef597936..d1d88b2a 100644 --- a/Test/dafny0/NestedPatterns.dfy +++ b/Test/dafny0/NestedPatterns.dfy @@ -69,7 +69,7 @@ method MethodG<T>(xs: List<T>) returns (xxs: List<List<T>>) case Cons(h, Cons(ht, tt)) =>
}
-method AssertionFailure(xs: List<T>)
+method AssertionFailure(xs: List)
{
match xs
case (Nil) => // BUG: this line causes an assertion in the Dafny implementation (what should happen is that "(Nil)" should not be allowed here)
@@ -100,7 +100,7 @@ method DuplicateIdentifierInPattern2<T>(xs: List<T>) case Cons(h, Cons(e, e)) => // BUG: here, the duplicate identifier is detected, but the error message is shown 3 times, which is less than ideal
}
-method Tuples0(xs: List<T>, ys: List<T>)
+method Tuples0(xs: List, ys: List)
{
match (xs, ys)
case (Nil, Nil) =>
@@ -110,14 +110,14 @@ method Tuples0(xs: List<T>, ys: List<T>) // only the identifiers in the last constructors are
}
-method Tuples1(xs: List<T>, ys: List<T>)
+method Tuples1(xs: List, ys: List)
{
match (xs, ys, 4)
case (Nil, Nil) => // BUG: the mismatch of 3 versus 2 arguments in the previous line and this line causes Dafny to crash with an
// assertion failure "mc.CasePatterns.Count == e.Arguments.Count"
}
-method Tuples2(xs: List<T>, ys: List<T>)
+method Tuples2(xs: List, ys: List)
{
match (xs, ys, ())
case (Nil, Nil, ()) => // BUG: Dafny crashes with an assertion failure "e.Arguments.Count >= 1"
diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy index 761cffa0..8c910959 100644 --- a/Test/dafny0/ResolutionErrors.dfy +++ b/Test/dafny0/ResolutionErrors.dfy @@ -1253,14 +1253,14 @@ module SignatureCompletion { datatype Dt = Ctor(X -> Dt) // error: X is not a declared type
datatype Et<Y> = Ctor(X -> Et, Y) // error: X is not a declared type
- // For methods and functions, signatures can auto-declare type parameters
- method My0(s: set, x: A -> B)
- method My1(x: A -> B, s: set)
+
+ method My0<A,B>(s: set, x: A -> B)
+ method My1<A,B>(x: A -> B, s: set)
method My2<A,B>(s: set, x: A -> B)
method My3<A,B>(x: A -> B, s: set)
- function F0(s: set, x: A -> B): int
- function F1(x: A -> B, s: set): int
+ function F0<A,B>(s: set, x: A -> B): int
+ function F1<A,B>(x: A -> B, s: set): int
function F2<A,B>(s: set, x: A -> B): int
function F3<A,B>(x: A -> B, s: set): int
}
|