| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
| |
clues about which parameters to include.
As a result, improved many test cases (see, e.g., dafny4/NipkowKlein-chapter7.dfy!) and beautified some others.
|
| |
|
|
|
|
| |
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.
|
| | |
|
| |
|
|
|
|
|
|
|
|
| |
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, 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).
|
| |\ |
|
| | | |
|
| | |\
| |/
|/| |
|
| | | |
|
| | | |
|
| |/
|
|
| |
opportunity to designate a good trigger.
|
| | |
|
| | |
|
| |
|
|
|
|
| |
sequences, or roll-it-yourself maps. Instead, use "nat", List, and "map".
Use VC splitting to combat performance issues.
|
| |
|
|
| |
to use it.
|
| | |
|
| | |
|
| |
|
|
|
|
| |
Issue 17 on dafny.codeplex.com.
Added information that allows multiset members to be unboxed as needed (mimicking what was already done for sets).
|
| |
|
|
|
|
|
| |
similar
to RingBufferAuto.dfy and ExtensibleArrayAuto.dfy, respectively, so that the effect
of {:autocontracts} is more easily seen.
|
| |
|
|
| |
the assign-such-that statement instead. For example: x :| x in S;
|
| | |
|
| |
|
|
| |
around the bound variables optional.
|
| | |
|
| | |
|
| |
|
|
| |
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
|
| | |
|
| | |
|
| | |
|
| |\ |
|
| | |
| |
| |
| | |
(in particular, codatatypes), Dafny needs to check this. In these changes, Dafny supports the "(==)" suffix to type parameters, infers that suffix in some cases, and enforces equality support in many places. Refinement and datatypes still need more attention in the Dafny implementation.
|
| |\| |
|
| | | |
|
| |/ |
|
| | |
|
| |
|
|
|
|
|
| |
not be compiled)
Dafny: improved :autocontracts heuristic for detecting "simple query method"
Dafny: fixed some bugs
|
| |
|
|
| |
specifications
|
| |
|
|
| |
.cs file with the new /spillTargetCode switch
|
| |
|
leino
Dan Rosén
Unknown
Rustan Leino
Unknown
Unknown