| 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.
|
| |\ |
|
| | |\ |
|
| | |/
|/| |
|
| | | |
|
| | |
| |
| |
| | |
Thanks Valentin for elucidating this issue!
|
| | |
| |
| |
| | |
and #module were not handled
|
| |/ |
|
| |
|
|
|
|
|
|
|
| |
The function IgnoreFuel in UnfoldingPerformance.dfy used to be lit-wrapped. It
shouldn't be, because its reads clause is non-empty. This is not a soundness
bug, but fixing it improves performance in cases where a function call would be
incorrectly unrolled.
Test case written by Rustan.
|
| |
|
|
|
|
|
|
|
| |
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.
|
| |/ |
|
| |
|
|
| |
+ a small fix in runTests.py
|
| |\
| |
| |
| |
| | |
This contains trigger related things under the autoTriggers flag (disabled by
default), and some bug-fixes and cleanups that are already enabled.
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| | |
Fixed resolution bug where some type arguments were not checked to have been determined.
Fixed resolution bugs where checking for equality-supporting types was missing.
|
| | | |
|
| | | |
|
| | |
| |
| |
| | |
Found by enabling auto-generated triggers and looking for failing tests
|
| | |
| |
| |
| | |
improved the error message reported to users
|
| | | |
|
| | | |
|
| | |
| |
| |
| | |
shadow other variables (Issue #86)
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| |/
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
i.e., how many times Z3 is permitted to unfold it's definition. The
new {:fuel} annotation can be added to the function itself, it which
case it will apply to all uses of that function, or it can overridden
within the scope of a module, function, method, iterator, calc, forall,
while, assert, or assume. The general format is:
{:fuel functionName,lowFuel,highFuel}
When applied as an annotation to the function itself, omit functionName.
If highFuel is omitted, it defaults to lowFuel + 1.
The default fuel setting for recursive functions is 1,2. Setting the fuel higher,
say, to 3,4, will give more unfoldings, which may make some proofs go through
with less programmer assistance (e.g., with fewer assert statements), but it may
also increase verification time, so use it with care. Setting the fuel to 0,0 is
similar to making the definition opaque, except when used with all literal arguments.
|
| |\ |
|
| | |
| |
| |
| | |
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
|
| | |
|
| |
|
|
| |
allows an improvement of the generated Boogie (which will be especially good soon, when reads-clause checking may change)
|
| |
|
|
|
| |
Window's batch doesn't recognize ";" as a command separator; lit has a
workaround for that, bu it's just as simple to do the right thing on our side.
|
| |\ |
|
| | | |
|
| |/ |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
function last<T>(xs: List<T>): T
requires xs != Nil
{
match xs
case Cons(y, Nil) => y
case Cons(y, Cons(z, zs)) => last(Cons(z, zs))
}
And
function minus(x: Nat, y: Nat): Nat
{
match (x, y)
case (Zero, _) => Zero
case (Suc(_), Zero) => x
case (Suc(a), Suc(b)) => minus(a, b)
}
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
leino
Clément Pit--Claudel
Michael Lowell Roberts
Bryan Parno