| 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.
|
| |
|
|
| |
between a module and its refinement base.
|
| |
|
|
| |
of "if" statements.
|
| |
|
|
| |
ENABLE_IRONDAFNY is defined but this isn't critical and will be addressed shortly.
|
| |
|
|
|
| |
The new error reporting system has a simpler interface, isn't tied to the
resolver, and contains error source information.
|
| | |
|
| |
|
|
|
| |
- fix for requirement inheritance in refinement.
- minimimally viable implementation of exclusive refinement feature.
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
| |
outside the module that declares it. The body is now visible across the module boundary. To contain the knowledge of the body inside the module, mark the function/predicate as 'protected'.
Semantics of 'protected':
* The definition (i.e., body) of a 'protected' function is not visible outside the defining module
* The idea is that inside the defining module, a 'protected' function may or may not be opaque. However, this will be easier to support once opaque/reveal are language primitives. Therefore, for the time being, {:opaque} is not allowed to be applied to 'protected' functions.
* In order to extend the definition of a predicate in a refinement module, the predicate must be 'protected'
* The 'protected' status of a function must be preserved in refinement modules
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
| |
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.
|
| |
|
|
| |
previous version and changes necessitated by recent parsing refactoring
|
| |
|
|
|
|
| |
Added string literals with various escapes--a subset of those supported in C# and similar languages, including the C# verbatim strings.
Previously, the "print" statement and custom attributes could support expression-or-string arguments; there is no longer a need to special-case these, so these arguments are now just expressions.
Fixed lack of operator resolution in custom attributes.
|
| |
|
|
| |
along with a backward-compatibility warning message if such declarations are attempted
|
| | |
|
| |\ |
|
| | |
| |
| |
| | |
Fixed bug in type checking for integer division.
|
| |/
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Now, loops that may possibly
do an infinite number of iterations (that is, loops marked with 'decreases *') and calls to methods
marked with 'decreases *' are allowed only in methods that themselves are marked with 'decreases *'. As
before, ghost loops and ghost methods are not allowed to be marked with 'decreases *'.
Previously, 'decreases *' was allowed on a method only if the method was tail recursive;
this is no longer so. Note, however, that if the method is not tail recursive and engages
in infinite recursion, then it will eventually run out of stack space.
Previously, a 'decreases *' was not inherited in a refining module; this is no longer so.
That is, 'decreases *' is now inherited. To refine a possibly non-terminating method
or loop, the refining version simply provides a decreases clause that does not mention '*'.
Note that if the refined method is not recursive, it still needs to have _some_ decreases
clause in order not to inherit the 'decreases *' from the refined method, but the expression
stated in the decreases clause can be arbitrary (for example, one can write 'decreases true'
or 'decreases 7' or 'decreases x' for some 'x' in scope).
Note, in the new design, a method needs to be declared with 'decreases *' if
it may recurse forever _or_ if it contains a possibly infinite loop.
Note that the absence of 'decreases *' on a loop does not mean the loop will
terminate, but it does mean that the loop will iterate a finite number of times
(the subtle distinction here is that a loop without a 'decreases *' is allowed
to contain a nested loop that has a 'decreases *' -- provided the enclosing
method is also declared with 'decreases *', as previously mentioned).
|
| |\ |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
* 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
|
| |/
|
|
|
|
| |
-possibility to declare traits in Dafny
-possibility to extend a class by a trait
-possibility to override body-less methods
|
| | |
|
| |
|
|
| |
Started allowing arbitrary types to have type parameters
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
refinement.
|
| |
|
|
| |
to VarDeclStmt.Locals
|
| |
|
|
| |
-> "prefix lemma")
|
| | |
|
| |
|
|
| |
like).
|
| |
|
|
| |
consistent with everything else), not the "iterator" keyword
|
| |
|
|
|
|
|
| |
VarDecl statements, there's often no good .EndTok information.)
Used the .EndTok in CaptureState information. In other words, move the blue dots in the IDE to after the statement just executed.
Removed /*!*/ comments in some parts of the source code -- CodeContracts reveal this information.
|
| | |
|
| |
|
|
| |
a "modifies" clause) and "colemma" (synonymous with "comethod"; perhaps "comethod" will go away at some point)
|
| |
|
|
| |
around the bound variables optional.
|
| |
|
|
|
| |
Fixed some precondition violations
Various improvements in Contracts
|
| |
|
|
| |
renamed "ghost module" to "abstract module", adding a keyword "abstract"
|
| |
|
|
|
|
| |
re-verifying the postcondition at that time
let refined classes inherit attributes
|
| | |
|
| |
|
|
|
|
|
| |
* Added "comethod" declarations and support for writing manual co-inductive proofs (but currently blindly assume comethod postconditions to, in positive positions, only have copredicates and codatatype equalities--other cases still need to be dealt with)
Code restructuring:
* New set of Boogie procedure stubs generated for each other
* Start of improvements around TrSplitExpr
|
| |
|
qunyanm
Michael Lowell Roberts
Clément Pit--Claudel
Dan Rosén
Reza Ahmadi
Bryan Parno
Rustan Leino