| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Fixed bug in BplImp! |  leino | 2015-07-01 |
| | | | | | Improvements in encoding of reads of function values. | ||
| * | Tried to reduce frame-axiom instantiations by saying the earlier heap must ↵ | leino | 2015-06-25 |
| | | | | | | | be a "heap anchor". Currently, a heap is an anchor if it produced by a havoc (but not a direct update). | ||
| * | Fix the Seq#Contain axiom; it should talk about T, not ref. |  Clément Pit--Claudel | 2015-06-07 |
| | | |||
| * | Add an infinite set collection type. | qunyanm | 2015-05-29 |
| | | |||
| * | Fixed some bugs in override axioms (but still missing support for classes ↵ | leino | 2015-04-05 |
| | | | | | | | | with type parameters). Resolve ClassDecl.TraitsTyp as types. Moved declaration of TraitParent and NoTraitAtAll to prelude. | ||
| * | Beefed up collection axioms (in particular, for maps) to improve the chance ↵ | Rustan Leino | 2015-03-10 |
| | | | | | of proving the existence check of let-such-that and assign-such-that | ||
| * | Removed some old and unused functions | leino | 2015-03-09 |
| | | |||
| * | Add imap display/update expressions | chrishaw | 2015-02-27 |
| | | |||
| * | Add imap type, which is like map but may have have infinite size | chrishaw | 2015-02-26 |
| | | |||
| * | Various DafnyPrelude.bpl cleanup. | leino | 2014-11-01 |
| | | | | | Removed unused cases from axioms where Seq#Take and Seq#Drop take out-of-range arguments | ||
| * | Improved power of axioms Seq#FromArray | leino | 2014-10-31 |
| | | |||
| * | Add an option to use reduce Z3's knowledge of non-linear arithmetic. |  Bryan Parno | 2014-10-24 |
| | | | | | Results in more manual work, but it also produces more predictable behavior. | ||
| * | Comparisons and well-founded order of char | leino | 2014-10-21 |
| | | |||
| * | Added types "char" and "string" (the latter being a synonym for "seq<char>"). | leino | 2014-10-20 |
| | | | | | | | Added string literals with various escapes--a subset of those supported in C# and similar languages, including the C# verbatim strings. Previously, the "print" statement and custom attributes could support expression-or-string arguments; there is no longer a need to special-case these, so these arguments are now just expressions. Fixed lack of operator resolution in custom attributes. | ||
| * | Fixed bugs in previous check-in | leino | 2014-08-25 |
| | | | | | Made up for inadequacy in reasoning machinery (supplying Int(Real(i)) == i axiom) | ||
| * | Added .Trunc field to real-based types | leino | 2014-08-21 |
| | | | | | Changed semantics of real-to-int conversions--these now have a precondition that the number converted is already an integer | ||
| * | Add higher-order-functions and some other goodies |  Dan Rosén | 2014-08-11 |
| | | | | | | | | | | | | | | | | | * The reads clause now needs to be self framing. * The requires clause now needs to be framed by the reads clause. * There are one-shot lambdas, with a single arrow, but they will probably be removed. * There is a {:heapQuantifier} attribute to quantifiers, but they will probably be removed. * Add smart handling of type variables * Add < and > for datatype & type parameter | ||
| * | Merge | Dan Rosén | 2014-07-07 |
| |\ | |||
| * | | New logical encoding of types with Is and IsAlloc | Dan Rosén | 2014-07-07 |
| | | | |||
| | * | Added some axioms about seq-to-multiset conversions | Rustan Leino | 2014-06-24 |
| | | | |||
| | * | Specialized Lit function for int and real (leaving all other cases ↵ | Rustan Leino | 2014-06-10 |
| | | | | | | | | | | | | | polymorphic). This reduces the number of int<->U conversions that Boogie adds, which avoids a looping problem in Z3. (Regrettably, the test suite seems to have become rather unstable. Sometimes everything verifies and sometimes there is some looping forever.) | ||
| | * | Improved axiom that knows that array-to-sequence converstion depends only on ↵ | Rustan Leino | 2014-06-04 |
| |/ | | | | those heap location that hold the array elements | ||
| * | Improvements in sequence axioms to make checking more automatic. | Rustan Leino | 2014-04-02 |
| | | | | | Minor changes in a test file. | ||
| * | Added axiom to transfer array element-type information onto the elements ↵ | Rustan Leino | 2014-03-20 |
| | | | | | | | themselves. Other serendipitous axiom improvements. | ||
| * | Fixed problem with propagating allocation information about array elements. | Rustan Leino | 2014-03-20 |
| | | | | | Improved situation with (reducing bogosity of) type checking of "object". | ||
| * | Removed an apparently unneeded trigger. | Rustan Leino | 2014-03-06 |
| | | |||
| * | Fix soundness bug (Issue #9 on dafny.codeplex.com) in function axiom for ↵ | Rustan Leino | 2014-02-13 |
| | | | | | | | literals. Added axiom to better handle DtAlloc/GenericAlloc correspondence (which improves handling of computations). | ||
| * | Preliminary support for reals in Dafny specs. No compiler suport yet. | Bryan Parno | 2014-02-10 |
| | | |||
| * | Print and translate "match" expressions in general positions, not just at ↵ | Rustan Leino | 2014-01-03 |
| | | | | | the top-level of function bodies. (Note, resolver also needs to allow this before the user can take advantage of this.) | ||
| * | Embellished axioms about GenericAlloc and DtAlloc. | Rustan Leino | 2014-01-03 |
| | | |||
| * | Unified function/method context heights | Rustan Leino | 2013-08-04 |
| | | |||
| * | Changed the encoding of recursive functions. Previous, three hardcoded ↵ | Rustan Leino | 2013-08-02 |
| | | | | | | | layers were used: F#2, F, and F#limited. Now, recursive functions take a layer argument, which is specified by Peano numbers. Also, cleaned up and made more consistent the emission of axioms regarding functions. | ||
| * | Axioms that relate (multi)set cardinality with (multi)set difference. | Rustan Leino | 2013-07-16 |
| | | | | | Removed three redundant multiset axioms. | ||
| * | Computations! |  Unknown | 2013-07-04 |
| | | | | | | | | Generates 'computing' axioms for both all formals and just decreasing formals. Supported are literal datatypes, booleans and numbers. The axioms are given a weight of 10, which seems enough for Z3 to give up when it is sane to do so. | ||
| * | Changed ranking function for Seq, so that it's compatible with data types. | Unknown | 2013-06-26 |
| | | |||
| * | Beefed up axioms about cardinality and the empty (multi)set, which fixes ↵ | Rustan Leino | 2013-06-20 |
| | | | | | | | Issue 17 on dafny.codeplex.com. Added information that allows multiset members to be unboxed as needed (mimicking what was already done for sets). | ||
| * | Removed the set cardinality/subset axiom (with no trigger, it caused test ↵ |  Rustan Leino | 2013-04-02 |
| | | | | | suite to fail; even with a restrictive trigger, it added a few minutes to the test suite) | ||
| * | Updated cardinality axioms for sets. |  Nadia Polikarpova | 2013-03-30 |
| | | |||
| * | The "choose" statement, hacky and specialized as it was, is now gone. Use ↵ | Rustan Leino | 2013-03-27 |
| | | | | | the assign-such-that statement instead. For example: x :| x in S; | ||
| * | First take on set, multiset and map cardinality. | Nadia Polikarpova | 2013-03-22 |
| | | |||
| * | Disallow allocations in ghost contexts | Rustan Leino | 2013-03-06 |
| | | |||
| * | Encode codatatype equalities by predefined copredicates, including their ↵ | Rustan Leino | 2013-01-15 |
| | | | | | prefix versions | ||
| * | Test cases for co-inductive proofs, and an axiom that makes some of them ↵ | Rustan Leino | 2012-10-19 |
| | | | | | possible | ||
| * | Added some axioms to try to recover boxed data. In particular, any element ↵ |  Unknown | 2012-10-17 |
| | | | | | 'x' of a set in the encoding satisfies Box(Unbox(x))==x. The soundness and performance of the axiomatization are dicey, so the axioms are made available only to method in-parameters. | ||
| * | Change the encoding of proof certificates to make the two levels explicit | Unknown | 2012-10-12 |
| | | | | | Restrict what conclusions comethods are allowed to have | ||
| * | New feature: | Rustan Leino | 2012-10-11 |
| | | | | | | | | * Added "comethod" declarations and support for writing manual co-inductive proofs (but currently blindly assume comethod postconditions to, in positive positions, only have copredicates and codatatype equalities--other cases still need to be dealt with) Code restructuring: * New set of Boogie procedure stubs generated for each other * Start of improvements around TrSplitExpr | ||
| * | Dafny: fixed merge | Rustan Leino | 2012-10-04 |
| | | |||
| * | Merge | Rustan Leino | 2012-10-04 |
| |\ | |||
| * | | Dafny: complete implementation of iterators | Rustan Leino | 2012-10-03 |
| | | | |||
| * | | Dafny: more part of verifying iterators | Rustan Leino | 2012-10-03 |
| | | | |||
 |
index : debian-dafny | |
| Debian packaging for Dafny |
| summaryrefslogtreecommitdiff |