| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
For the following situation
module LibA {
// ...things declared here...
}
module LibB {
// ...things declared here...
}
module R {
import opened LibA
// ...things declared here...
}
module S refines R {
import opened LibB
// ...declared here...
}
1. If module R declares a TopLevelDecl “G”, then we should report an error if S
attempts to declare an incompatible TopLevelDecl “G”. Dafny does this already.
2. If LibA declares a TopLevelDecl “G” but R does not directly declare any
TopLevelDecl G”, then we should also issue an error for any TopLevelDecl “G”
in S. This behavior is missing in Dafny.
3. If each of LibA and LibB declares some TopLevelDecl “G”, but neither R nor S
directly declares any TopLevelDecl “G”, then no error should be issued, and
any use of “G” in S should resolve to the “G” in LibA. This behavior is missing
in Dafny.
|
| |
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
| |
a module import.
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
|
|
|
| |
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.
|
| | |
|
| |
|
|
| |
now created by the parser into the system module.
|
| | |
|
| | |
|
| |
|
qunyanm
Clément Pit--Claudel
Michael Lowell Roberts
Dan Rosén