| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
| |
derived these predicates. More things can now be verified (including the
problem reported in Issue #49).
|
| |
|
|
| |
Moved all bounds discovery to resolution pass 1.
|
| |
|
|
|
|
|
|
|
| |
Dafny counts from 0, but Boogie counts from 1. Tokens are 1-based. Thus when we
print tokens, we need to decrement the column number. This was done for resolver
errors, but not for verification or parsing errors. In addition, parsing errors
were inconsistent with resolution errors case-wise.
Unfortunately, the fix affects the output of many tests.
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| | |
|
| | |
|
| |
|
|
| |
currently unused in the test suite)
|
| |
|
|
|
| |
can now assume the precondition (as had also been the case back in the days when
reads clauses had to be self framing).
|
| |
|
|
|
|
| |
Test/dafny0/Reads.dfy for benefits.
(Unfortunately, this loses track of the "postcondition might not hold on this return path" locations, see Test/dafny0/FunctionSpecifications.dfy.)
|
| |
|
|
| |
precondition has otherwise been checked for well-formedness
|
| |
|
|
| |
corresponding incorrectly recorded desired answer)
|
| | |
|
| |
|
|
| |
provable.
|
| | |
|
| |
|
|
|
|
|
| |
so use the new name resolution machinery that handles modules and type parameters
Included some inadvertently left-out test cases in dafny0/Modules0.dfy
Fixed comparable-types tests
|
| |
|
|
|
|
|
|
|
|
| |
class are now
automatically static, and fields are no longer allowed to be declared there. Stated
differently, all heap state must now be declared inside an explicitly declared class,
and functions and methods declared outside any class can be viewed as belonging to
the module. The motivating benefit of this change is to no longer need the 'static'
keyword when declaring a module of functions and methods.
|
| |
|
|
| |
Removed now defunct IdentifierSequence from the AST.
|
| | |
|
| |
|
|
| |
expression.
|
| |
|
|
| |
declarations
|
| |
|
|
| |
consists of one tuple type.
|
| |
|
|
|
|
| |
Renamed "default constructor" to "anonymous constructor" (since there's really nothing "default" about it).
If the type of literal "null" is unresolved, make the type "object".
The need to translate unresolved proxies is now assumed to be gone.
|
| |
|
|
| |
now created by the parser into the system module.
|
| |
|
|
|
| |
Arbitrary conversion from int/real to derived types not yet supported.
Changed rules about numeric type conversions to allow conversions from any numeric type.
|
| |
|
|
| |
+ add a test case with lambdas that don't get their types fully specified
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
twoState and codeContext is moved to a new class ResolveOpts
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
|
|
* The reads clause now needs to be self framing.
* The requires clause now needs to be framed by the reads clause.
* There are one-shot lambdas, with a single arrow, but they will probably be
removed.
* There is a {:heapQuantifier} attribute to quantifiers, but they will
probably be removed.
* Add smart handling of type variables
* Add < and > for datatype & type parameter
|
Rustan Leino
Clément Pit--Claudel
Dan Rosén