From e10098cde7bac9a7a1576000fa29d15f1fcd8970 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Thu, 2 Jul 2015 16:06:02 -0700 Subject: 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. --- Test/hofs/ResolveError.dfy.expect | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'Test/hofs/ResolveError.dfy.expect') diff --git a/Test/hofs/ResolveError.dfy.expect b/Test/hofs/ResolveError.dfy.expect index c3e0c242..11471ffd 100644 --- a/Test/hofs/ResolveError.dfy.expect +++ b/Test/hofs/ResolveError.dfy.expect @@ -2,8 +2,8 @@ ResolveError.dfy(86,6): Error: RHS (of type ((int,bool)) -> real) not assignable ResolveError.dfy(91,15): Error: incorrect type of method in-parameter 0 (expected ? -> ?, got (int,bool) -> real) ResolveError.dfy(101,6): Error: RHS (of type (()) -> real) not assignable to LHS (of type () -> real) ResolveError.dfy(102,6): Error: RHS (of type () -> real) not assignable to LHS (of type (()) -> real) -ResolveError.dfy(7,11): Error: the number of left-hand sides (1) and right-hand sides (2) must match for a multi-assignment -ResolveError.dfy(8,11): Error: the number of left-hand sides (1) and right-hand sides (2) must match for a multi-assignment +ResolveError.dfy(7,9): Error: the number of left-hand sides (1) and right-hand sides (2) must match for a multi-assignment +ResolveError.dfy(8,9): Error: the number of left-hand sides (1) and right-hand sides (2) must match for a multi-assignment ResolveError.dfy(21,6): Error: LHS of assignment must denote a mutable field ResolveError.dfy(31,16): Error: arguments must have the same type (got int and bool) ResolveError.dfy(32,12): Error: wrong number of arguments to function application (function type 'int -> int' expects 1, got 2) @@ -17,7 +17,7 @@ ResolveError.dfy(39,18): Error: wrong number of arguments to function applicatio ResolveError.dfy(46,15): Error: a reads-clause expression must denote an object or a collection of objects (instead got int) ResolveError.dfy(47,7): Error: Precondition must be boolean (got int) ResolveError.dfy(56,9): Error: condition is expected to be of type bool, but is () -> bool -ResolveError.dfy(59,34): Error: arguments must have the same type (got A -> B and ?) +ResolveError.dfy(59,39): Error: arguments must have the same type (got A -> B and ?) ResolveError.dfy(62,11): Error: arguments must have the same type (got A -> B and object) ResolveError.dfy(68,24): Error: unresolved identifier: _ 22 resolution/type errors detected in ResolveError.dfy -- cgit v1.2.3