| Commit message (Expand) | Author | Age |
* | Fixed some bugs in override axioms (but still missing support for classes wit... | leino | 2015-04-05 |
* | Beefed up collection axioms (in particular, for maps) to improve the chance o... | Rustan Leino | 2015-03-10 |
* | 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 |
* | 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 |
* | 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 |
* | Fixed bugs in previous check-in | leino | 2014-08-25 |
* | Added .Trunc field to real-based types | leino | 2014-08-21 |
* | Add higher-order-functions and some other goodies | Dan Rosén | 2014-08-11 |
* | 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 polymorphi... | Rustan Leino | 2014-06-10 |
| * | Improved axiom that knows that array-to-sequence converstion depends only on ... | Rustan Leino | 2014-06-04 |
|/ |
|
* | Improvements in sequence axioms to make checking more automatic. | Rustan Leino | 2014-04-02 |
* | Added axiom to transfer array element-type information onto the elements them... | Rustan Leino | 2014-03-20 |
* | Fixed problem with propagating allocation information about array elements. | Rustan Leino | 2014-03-20 |
* | Removed an apparently unneeded trigger. | Rustan Leino | 2014-03-06 |
* | Fix soundness bug (Issue #9 on dafny.codeplex.com) in function axiom for lite... | Rustan Leino | 2014-02-13 |
* | 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 the... | Rustan Leino | 2014-01-03 |
* | 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 layer... | Rustan Leino | 2013-08-02 |
* | Axioms that relate (multi)set cardinality with (multi)set difference. | Rustan Leino | 2013-07-16 |
* | Computations! | Unknown | 2013-07-04 |
* | 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 Issu... | Rustan Leino | 2013-06-20 |
* | Removed the set cardinality/subset axiom (with no trigger, it caused test sui... | Rustan Leino | 2013-04-02 |
* | Updated cardinality axioms for sets. | Nadia Polikarpova | 2013-03-30 |
* | The "choose" statement, hacky and specialized as it was, is now gone. Use th... | Rustan Leino | 2013-03-27 |
* | 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 pref... | Rustan Leino | 2013-01-15 |
* | Test cases for co-inductive proofs, and an axiom that makes some of them poss... | Rustan Leino | 2012-10-19 |
* | Added some axioms to try to recover boxed data. In particular, any element '... | Unknown | 2012-10-17 |
* | Change the encoding of proof certificates to make the two levels explicit | Unknown | 2012-10-12 |
* | New feature: | Rustan Leino | 2012-10-11 |
* | 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 |
* | | Dafny: incomplete snapshot of verification of iterators | Rustan Leino | 2012-10-02 |
| * | Dafny: removed div/mod axioms, since Boogie now interprets div/mod | Unknown | 2012-09-28 |
| * | Boogie: new syntax for integer division and modulus: use div and mod instead ... | boehmes | 2012-09-27 |
|/ |
|
* | Dafny: things about sequences: parse Suffix expressions after DisplayExpr's, ... | Unknown | 2012-09-12 |