| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
|
|
| |
* Set Z3's QI_COST as the sum of "weight" and "generation", not their product. This worked better when setting the :weight of a quantifier (see below).
Dafny:
* Improved axiomatization of sequences; in particular, use an axiom to generate terms that say what the two pieces of a concatenation are
* Two of the (previous) sequence axioms could cause a matching loop, in cases where Z3's arithmetic reasoning does not infer all rational arithmetic equalities during instantiation. The effect of this was apparently not noticed before, perhaps the concatenation/drop properties previously had to be supplied in manual assert statements. But now, with the improved sequence axiomatization (see previous bullet), this effect became remarkably noticeable. To reduce the bad effect of this apparent matching loop, Michal and I added a :weight annotation on two of the axioms, which, along with the Boogie change above, seems to give acceptable results.
* Removed several assert lemmas that are no longer needed in Test programs (the test programs now contain only about a handful of such lemmas)
|
| |
|
|
|
|
| |
* Added some more set axioms that go "inside out" for union and set differences (UnionOne already had such an axiom)
* Fixed bug to, once again, allow multiple .dfy files on the command line (with the effect of them being merged into one program)
* Fixed bug in translation of reads/modifies clauses that mention sequences
|
| |
|
|
|
|
|
| |
* Added arrays
* Beefed up set axiomatization to know more things about set displays
* Added a simple heuristic that can infer some simple decreases clauses for loops
* Added Dafny solutions to a couple of VACID benchmarks
|
| | |
|
| |
|
|
|
| |
* Effectively make all in- and out-parameters of ghost methods ghosts.
* Added DafnyRuntime.cs back in, which is needed to run Dafny programs, but which, unfortunately, is currently not being used in the test suite (something we should address)
|
| |
|
|
| |
svn-added files are ignored. Currently added are only the files that are not generated during the build process (e.g. Makefile, FSharp.Core.dll), hence all files generated during the build process won't be committed.
|
| |
|
|
|
| |
* Recoded frame axioms to be more goal directed
* Added Main test driver to Test/VSI-Benchmarks/b2.dfy
|
| |
|
|
|
|
|
|
| |
* First crack at a compiler (/compile:1 writes out.cs, if Dafny program verifies)
* Added "print" statement (to make running compiled programs more interesting)
* Changed name of default class from $default to _default
Boogie:
* Included "lambda" as a keyword in emacs and latex style files
|
| |
|
|
|
|
|
| |
* Added match statements (in addition to the previous match expressions)
* Added missing axiom about boxes and datatypes
* Improved axioms for datatype rank comparisons
* Added test cases with mutual-recursion termination challenges
|
| |
|
|
| |
consistency is being checked.
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
| |
boolean-only if-then-else expressions)
Dafny: Added 'class' functions and methods (i.e., functions and methods with a receiver parameter)
Dafny grammar changes: Tthe 'use' keyword now goes before 'function' (akin to 'ghost' and 'class'), and quantifier triggers now go before the '::'
Dafny: Check for division-by-zero for both '/' and '%'
|
| | |
|
| |
|
|
|
|
| |
bodies) match expressions.
Addressed a couple of todos, including checking the well-formedness of quantifiers and if-then-else expressions in function bodies.
|
| |
|
|
| |
Included VSI-Benchmarks in standard tests.
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
| |
and seq.
Regrettably, these changes--although improvements in Dafny's functionality--have caused Test/dafny0/BinaryTree.bpl and Test/dafny0/SchorrWaite.dfy to be significantly slower (the dafny0 test directory now takes 6:11 whereas it used to take 1:43).
Improved some of the VSI-Benchmarks to use generics more fully, where the previous designed had just crashed.
Included the previously commented-out loop invariants and assertions in VSI-Benchmarks/b8.dfy.
Added a space in the pretty printing of Boogie coercion expressions.
|
| |
|
|
| |
sequences (for both Dafny and Chalice). This in turn fixes issue 5876.
|
| | |
|
| | |
|
| |
|
|
| |
Deleted/ignored some binaries in the Binaries directory.
|
| |
|
|
|
| |
Dafny: Make use of function preconditions in function well-definedness checks.
Chalice: Changed old "install" to current "reorder" keyword in Emacs mode.
|
| |
|
|
|
|
|
|
| |
* Added DeclType(f)==C axioms, which for each field f says which class declares it.
Boogie:
* Changed behavior of free loop invariants. Now, a free loop invariant is ignored on the checking side, just like for free requires and free ensures. The new switch /alwaysAssumeFreeLoopInvariants flag gives the previous behavior.
* NOTE: I did NOT yet make the corresponding change for loop unrolling, but it is needed.
|
| | |
|
| |
|
|
| |
Boogie.
|
| |
|
|
| |
and not just the LKG.
|
| |
|
rustanleino