| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| | |
|
| |\ |
|
| | |
| |
| |
| | |
Improvements in encoding of reads of function values.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| | | |
|
| |/ |
|
| |\ |
|
| | |
| |
| |
| |
| |
| | |
be a "heap anchor".
Currently, a heap is an anchor if it produced by a havoc (but not a direct update).
|
| | |
| |
| |
| | |
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
|
| | |
|
| |\ |
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
The problem was this:
Console.WriteLine(Int64.Parse("08000000000000000", NumberStyles.HexNumber));
// => -9223372036854775808
Console.WriteLine(Int64.Parse("9223372036854775808"));
// => Value was either too large or too small for an Int64.
In other words, large hex numbers are interpreted as a sequence of bits, not as
an actual number.
|
| |\| |
|
| | |
| |
| |
| | |
allows an improvement of the generated Boogie (which will be especially good soon, when reads-clause checking may change)
|
| | |\ |
|
| | | | |
|
| | | |\
| | |/
| |/| |
|
| | |/
|/| |
|
| | | |
|
| | | |
|
| |/ |
|
| |
|
|
|
| |
The test suite relies on error codes all being zero (except for preprocessing
errors), so add a flag for that (as suggested in a source comment).
|
| |
|
|
|
| |
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.
|
| |
|
|
|
|
|
|
|
|
|
|
| |
runTests.py reads lit-style annotations, so we will be able to retain lit
compatibility. This new framework adds:
* Precise timings
* Proper support for interrupting using Ctrl+C
* Much better reporting (including tracking of error codes, and merging
of successive reports for performance tracking)
* No dependency on lit, OutputCheck, or Diff
* Pretty colors!
|
| | |
|
| |\ |
|
| | | |
|
| | | |
|
| |/
|
|
| |
need for Total
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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)
}
|
| |
|
|
|
|
| |
Fix bug with not seeing imap's because of type synonyms.
Don't show semi-colon after "decreases" in hover text.
Minor cosmetic change in a test case.
|
| |
|
|
|
|
| |
Klein book on semantics.
It includes many uses of inductive predicates and inductive lemmas.
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
corresponding incorrectly recorded desired answer)
|
| | |
|
| |
|
|
| |
provable.
|
| |
|
|
| |
Klein book on semantics
|
Rustan Leino
Bryan Parno
Clément Pit--Claudel
Michael Lowell Roberts