| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Language change: All functions and methods declared lexically outside any ↵ |  leino | 2014-12-12 |
| | | | | | | | | | | | 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. | ||
| * | New logical encoding of types with Is and IsAlloc |  Dan Rosén | 2014-07-07 |
| | | |||
| * | Set up the same test infrastructure as in Boogie. | wuestholz | 2014-05-29 |
| | | |||
| * | Dafny: retired the "call" keyword |  Rustan Leino | 2011-05-26 |
| | | |||
| * | Boogie: | rustanleino | 2010-06-22 |
| | | | | | | | | | | * 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) | ||
| * | Dafny: Added two additional heuristics for guessing missing loop decreases ↵ | rustanleino | 2010-06-11 |
| | | | | | clauses (for loop guard A!=B and for loop guards with multiple conjuncts) | ||
| * | Dafny: | rustanleino | 2010-05-21 |
| * 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 | |||
 |
index : debian-dafny | |
| Debian packaging for Dafny |
| summaryrefslogtreecommitdiff |