| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
| |
We already have separate tests for those, and we want the output to be the same
with and without /autoTriggers.
|
| |
|
|
|
|
|
|
|
|
| |
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.
|
| |\ |
|
| | | |
|
| |/ |
|
| | |
|
| |
|
|
| |
to use it.
|
| |
|
|
| |
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
|
| | |
|
| |\ |
|
| | | |
|
| | |
| |
| |
| | |
(i.e. a != b is allowed when a: array<int> and b: array<T>)
|
| |/ |
|
| |
|
|
| |
.cs file with the new /spillTargetCode switch
|
| | |
|
| |
|
|
| |
avoid clashes with C# keywords, added switch in runtest scripts to turn on compilation
|
| |
|
|
| |
assignments where RHS is not just an expression
|
| |
|
|
|
|
|
|
|
|
|
| |
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);
|
| |
|
|
|
|
| |
* Added full support for multi-dimensional arrays (except for one issue that still needs to be added in compilation)
* Changed syntax of array length from |a| to a.Length (for one-dimensional arrays). The syntax for either dimensions is, for example, b.Length0 and b.Length1 for 2-dimensional arrays.
* Internally, this meant adding support for built-in classes and readonly fields
|
| |
|
|
|
|
|
|
|
| |
* 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)
|
| |
|
|
| |
clauses (for loop guard A!=B and for loop guards with multiple conjuncts)
|
| |
|
|
|
|
| |
* Fixed bug in translation of well-formedness conditions
* Added Test/dafny0/Celebrity.dfy
* Added a harness to Test/vacid0/Composite.dfy
|
|
|
* 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
|
Clément Pit--Claudel
leino
Dan Rosén
Rustan Leino
Unknown
Unknown