| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
| |
be a "heap anchor".
Currently, a heap is an anchor if it produced by a havoc (but not a direct update).
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
| |
- replaced the sequences used to specify permutations with multisets
- used some of the newer syntax in Dafny
|
| |
|
|
| |
body-less functions/methods
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
| |
syntax. What you previously would have written like:
c := new C;
call c.Init(x, y);
you can now write as:
c := new C.Init(x, y);
|
| |
|
|
|
|
|
|
|
| |
* 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)
|
| |
|
|
|
| |
* changed implementation of Test/VSI-Benchmarks/b4.dfy to be more interesting (and, in particular, different from the specification)
* reformatted Test/VSI-Benchmarks/b3.dfy
|
| |
|
|
| |
clauses (for loop guard A!=B and for loop guards with multiple conjuncts)
|
| |
|
|
|
|
|
| |
* 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
|
| |
|
|
|
|
| |
missing)
Boogie: Added {:subsumption <n>} attribute to assert statements, which overrides the /subsumption command-line setting
|
| |
|
|
|
| |
* Modifies clause checking is now done with each update, instead of at the end of the method. Not only does this improve error messages, but on some examples, it gives a dramatic speed-up (2x) in proving time.
* bugfix: range expressions of foreach statements were previously ignored during Translation
|
| |
|
|
|
|
| |
* Enforce ghost vs. non-ghost separation
* Allow ghost parameters and ghost locals
* Functions are ghost, but allow the non-ghost "function method"
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
| |
variables, if they were not already local variables.
|
| |
|
leino
Rustan Leino