| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
| |
it. Don't use pretty warning signs since we can't diff them correctly in the
test output from the test run.
|
| |
|
|
| |
protected predicated in cross-module calls) like in other places.
|
| |
|
|
|
|
| |
The issues here are mostly with induction (wrt. to trigger selection and
quantifier splitting) and with expressions like P(i, j-1) where no good choices
are available.
|
| |
|
|
|
| |
We already have separate tests for those, and we want the output to be the same
with and without /autoTriggers.
|
| |
|
|
|
|
| |
time) in the test suite.
Removed some assertions that have been rendered unnecessary because of the computations that Dafny instructs the SMT solver to do.
|
| |
|
|
|
|
|
|
|
| |
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.
|
| | |
|
| |
|
|
| |
Found by enabling auto-generated triggers and looking for failing tests
|
| |
|
|
|
|
|
|
|
|
| |
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
|
| | |
|
| |
|
|
|
|
|
|
|
|
| |
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.
|
| | |
|
| |
|
|
| |
of time :)
|
| |
|
|
| |
some brittleness
|
| | |
|
| | |
|
| |
|
|
| |
along with a backward-compatibility warning message if such declarations are attempted
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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
|
| |
|
|
| |
Cleaned up file to use some improved Dafny constructs.
|
| |\ |
|
| | | |
|
| | | |
|
| | | |
|
| |/ |
|
| | |
|
| | |
|
| |
|
|
| |
to use it.
|
| | |
|
| | |
|
| |
|
|
|
|
|
| |
where more type information is known
Refactored ConcreteUpdateStatement to no longer inherit from ConcreteSyntaxStatement.
Fixed numerous places where some recursive checks did not reach.
|
| |
|
|
| |
around the bound variables optional.
|
| | |
|
| | |
|
| |\ |
|
| | | |
|
| |/ |
|
| |
|
|
| |
renamed "ghost module" to "abstract module", adding a keyword "abstract"
|
| | |
|
| | |
|
| |
|
|
| |
Changed the test output to make it easier to spot (in the console output) that everything passed with success or if there were any failures
|
| |
|
|
|
|
| |
Iter.dfy!)
Fixed migration issues
|
| | |
|
| |
|
|
| |
from dafny2/Calculations, as it actually belongs in dafny0.
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
method calls
|
| | |
|
qunyanm
Clément Pit--Claudel
Dan Rosén
Nadia Polikarpova
Rustan Leino
Unknown